-- The fixed point theorem on a closed interval: a continuous map from
-- [A, B] into itself has a fixed point, by the intermediate value theorem
-- applied to the displacement X − f(X)
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.FixedPoint.Interval
import Real.Analysis.IntermediateValue

-- X ↦ X − f(X), built from the pointwise operations.
def displacement (f : Set) : Set :=
  pointwiseAdd(identity(ℝ), pointwiseMul(constantFunction(ℝ, ℝ, -(1:R)), f))

theorem displacement.value (f : Set) (X : Real)
  requires fFunction : f : ℝ → ℝ
  shows displacement(f)(X) = X - f(X)
proof
  have realX : X ∈ ℝ by simp [Real]
  have negOne : -(1:R) ∈ ℝ by typecheck
  have cFunction := constantFunction.function at ℝ, ℝ, -(1:R) with negOne
  have idFunction := identity.function at ℝ
  have mulFunction := pointwiseMul.function with cFunction, fFunction
  have fValue := FunctionBetween.apply_closed with fFunction, realX
  have cValue := constantFunction.apply with realX, negOne
  have idValue := identity.apply with realX
  have mulValue := pointwiseMul.value with cFunction, fFunction
  have mulClosed := FunctionBetween.apply_closed with mulFunction, realX
  have addValue := pointwiseAdd.value with idFunction, mulFunction
  simp [displacement]
  ring

theorem closedInterval.fixed_point (f : Set) (A B : Real)
  requires ordered : A ≤ B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires maps : ∀ X ∈ closedInterval(A, B), f(X) ∈ closedInterval(A, B)
  shows ∃ C ∈ closedInterval(A, B), f(C) = C
proof
  have fFunction := continuous.left
  have subset := closedInterval.subset_reals at A, B
  have negOne : -(1:R) ∈ ℝ by typecheck
  have constantContinuous := UniformContinuousOn.continuous_on with (constantFunction.uniform_continuous_on at closedInterval(A, B), -(1:R) with subset)
  have identityContinuous := closedInterval.identity_continuous at A, B
  have productContinuous := ContinuousOn.mul with constantContinuous, continuous
  have continuousD : ContinuousOn(displacement(f), closedInterval(A, B))
    unfold displacement
    exact ContinuousOn.add with identityContinuous, productContinuous
  have leftIn := closedInterval.left_mem with ordered
  have rightIn := closedInterval.right_mem with ordered
  obtain ⟨fAReal, fALower, fAUpper⟩ := closedInterval.membership.forward with (maps with A, leftIn)
  obtain ⟨fBReal, fBLower, fBUpper⟩ := closedInterval.membership.forward with (maps with B, rightIn)
  have dA := displacement.value at f, A with fFunction
  have dB := displacement.value at f, B with fFunction
  have below : (displacement(f)(A):R) ≤ 0
    rw dA
    linarith
  have above : (0:R) ≤ displacement(f)(B)
    rw dB
    linarith
  obtain ⟨C, hC, zero⟩ := closedInterval.intermediate_value_le with ordered, continuousD, below, above
  obtain ⟨realC, lowerC, upperC⟩ := closedInterval.membership.forward with hC
  have dC := displacement.value at f, C with fFunction
  rw dC at zero
  witness C
  refine ⟨hC, ?_⟩
  have fCReal := FunctionBetween.apply_closed with fFunction, realC
  linarith