Grace/Cumulus/FixedPoint/Interval.g17

Open in Workbench Download source

Imports

Real.Analysis.IntermediateValue

Declarations

Source

1-- The fixed point theorem on a closed interval: a continuous map from2-- [A, B] into itself has a fixed point, by the intermediate value theorem3-- applied to the displacement X − f(X)4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.FixedPoint.Interval10import Real.Analysis.IntermediateValue1112-- X ↦ X − f(X), built from the pointwise operations.13def displacement (f : Set) : Set :=14  pointwiseAdd(identity(ℝ), pointwiseMul(constantFunction(ℝ, ℝ, -(1:R)), f))1516theorem displacement.value (f : Set) (X : Real)17  requires fFunction : f : ℝ → ℝ18  shows displacement(f)(X) = X - f(X)19proof20  have realX : X ∈ ℝ by simp [Real]21  have negOne : -(1:R) ∈ ℝ by typecheck22  have cFunction := constantFunction.function at ℝ, ℝ, -(1:R) with negOne23  have idFunction := identity.function at ℝ24  have mulFunction := pointwiseMul.function with cFunction, fFunction25  have fValue := FunctionBetween.apply_closed with fFunction, realX26  have cValue := constantFunction.apply with realX, negOne27  have idValue := identity.apply with realX28  have mulValue := pointwiseMul.value with cFunction, fFunction29  have mulClosed := FunctionBetween.apply_closed with mulFunction, realX30  have addValue := pointwiseAdd.value with idFunction, mulFunction31  simp [displacement]32  ring3334theorem closedInterval.fixed_point (f : Set) (A B : Real)35  requires ordered : A ≤ B36  requires continuous : ContinuousOn(f, closedInterval(A, B))37  requires maps : ∀ X ∈ closedInterval(A, B), f(X) ∈ closedInterval(A, B)38  shows ∃ C ∈ closedInterval(A, B), f(C) = C39proof40  have fFunction := continuous.left41  have subset := closedInterval.subset_reals at A, B42  have negOne : -(1:R) ∈ ℝ by typecheck43  have constantContinuous := UniformContinuousOn.continuous_on with (constantFunction.uniform_continuous_on at closedInterval(A, B), -(1:R) with subset)44  have identityContinuous := closedInterval.identity_continuous at A, B45  have productContinuous := ContinuousOn.mul with constantContinuous, continuous46  have continuousD : ContinuousOn(displacement(f), closedInterval(A, B))47    unfold displacement48    exact ContinuousOn.add with identityContinuous, productContinuous49  have leftIn := closedInterval.left_mem with ordered50  have rightIn := closedInterval.right_mem with ordered51  obtain ⟨fAReal, fALower, fAUpper⟩ := closedInterval.membership.forward with (maps with A, leftIn)52  obtain ⟨fBReal, fBLower, fBUpper⟩ := closedInterval.membership.forward with (maps with B, rightIn)53  have dA := displacement.value at f, A with fFunction54  have dB := displacement.value at f, B with fFunction55  have below : (displacement(f)(A):R) ≤ 056    rw dA57    linarith58  have above : (0:R) ≤ displacement(f)(B)59    rw dB60    linarith61  obtain ⟨C, hC, zero⟩ := closedInterval.intermediate_value_le with ordered, continuousD, below, above62  obtain ⟨realC, lowerC, upperC⟩ := closedInterval.membership.forward with hC63  have dC := displacement.value at f, C with fFunction64  rw dC at zero65  witness C66  refine ⟨hC, ?_⟩67  have fCReal := FunctionBetween.apply_closed with fFunction, realC68  linarith69