-- Real analysis: FTCFirst
-- 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.Real.Analysis.Integration.FTCFirst
import IntegralOrderBound
import IndefiniteIntegral
import Differentiation
import RiemannSums
import CommonRefinementComparison
import MeanValueIntegration
import ContinuousIntegral

-- Section: FTCFirst
theorem integralFrom.secant_right (f : Set) (A B X Y H I : Real)
  requires ordered : A ≤ B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires left : A < X
  requires middle : X < Y
  requires right : Y ≤ B
  requires position : Y = X + H
  requires local : HasRiemannIntegral(f, X, Y, I)
  shows differenceQuotient(integralFrom(f, A, B), X)(H) = I / (Y - X)
proof
  have function := integralFrom.function with ordered, continuous
  have value := differenceQuotient.value at integralFrom(f, A, B), X, H with function
  have realX : X ∈ ℝ by simp [Real]
  have realY : Y ∈ ℝ by simp [Real]
  have fx := FunctionBetween.apply_closed with function, realX
  have fy := FunctionBetween.apply_closed with function, realY
  have increment := integralFrom.increment_right with ordered, continuous, left, middle, right, local
  have numerator : integralFrom(f, A, B)(Y) -
      integralFrom(f, A, B)(X) = I
    rw increment
    ring
  have width : Y - X = H
    rw position
    ring
  rw [← position, numerator] at value
  rwa width

theorem integralFrom.secant_left (f : Set) (A B X Y H I : Real)
  requires ordered : A ≤ B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires left : A < Y
  requires middle : Y < X
  requires right : X ≤ B
  requires position : Y = X + H
  requires local : HasRiemannIntegral(f, Y, X, I)
  shows differenceQuotient(integralFrom(f, A, B), X)(H) = I / (X - Y)
proof
  have function := integralFrom.function with ordered, continuous
  have value := differenceQuotient.value at integralFrom(f, A, B), X, H with function
  have realX : X ∈ ℝ by simp [Real]
  have realY : Y ∈ ℝ by simp [Real]
  have fx := FunctionBetween.apply_closed with function, realX
  have fy := FunctionBetween.apply_closed with function, realY
  have increment := integralFrom.increment_left with ordered, continuous, left, middle, right, local
  have numerator : integralFrom(f, A, B)(Y) -
      integralFrom(f, A, B)(X) = -I
    rw increment
    ring
  have width : H = -(X - Y)
    rw position
    ring
  have positive := realLess.implies_le with middle
  have widthPositive : 0 < X - Y by linarith
  have widthNonzero : X - Y ≠ realZero
    intro equal
    have strict := realLess.characterization.forward with widthPositive
    rw equal at strict
    exact RealLess.irreflexive with strict
  have negBoth := realDiv.neg_both at I, X - Y with widthNonzero
  rw [← position, numerator, width, negBoth] at value
  rwa width

-- A negative step H with X + H still inside [A, B] and -H below the local
-- control radius: the secant of the integral function over [X + H, X] is an
-- average of f within E of f(X).
theorem integralFrom.secant_bounds_left (f : Set) (A B X E D H : Real)
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires inside : X ∈ closedInterval(A, B)
  requires ordered : A ≤ B
  requires right : X ≤ B
  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →
    f(X) - E < (f(Z):R) ∧ (f(Z):R) < f(X) + E
  requires negative : H < 0
  requires above : A < X + H
  requires small : -H < D
  shows f(X) - E ≤ differenceQuotient(integralFrom(f, A, B), X)(H) ∧
    differenceQuotient(integralFrom(f, A, B), X)(H) ≤ f(X) + E
proof
  have below : X + H < X by linarith
  have aLeY := realLess.implies_le with above
  have width : X - (X + H) < D by linarith
  have restricted := ContinuousOn.subinterval with continuous, aLeY, right
  obtain ⟨J, realJ, integral⟩ := ContinuousOn.integrable_positive with below, restricted
  have average := ContinuousOn.left_integral_average with
    continuous, inside, control, below, aLeY, width, integral
  have position : X + H = X + H by rfl
  have secant := integralFrom.secant_left with ordered, continuous, above, below, right, position, integral
  rwa ← secant at average

-- The mirror image for a positive step.
theorem integralFrom.secant_bounds_right (f : Set) (A B X E D H : Real)
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires inside : X ∈ closedInterval(A, B)
  requires ordered : A ≤ B
  requires left : A < X
  requires control : ∀ Z ∈ closedInterval(A, B), dist(X, Z) < D →
    f(X) - E < (f(Z):R) ∧ (f(Z):R) < f(X) + E
  requires positive : 0 < H
  requires below : X + H < B
  requires small : H < D
  shows f(X) - E ≤ differenceQuotient(integralFrom(f, A, B), X)(H) ∧
    differenceQuotient(integralFrom(f, A, B), X)(H) ≤ f(X) + E
proof
  have weakLeft := realLess.implies_le with left
  have above : X < X + H by linarith
  have yLeB := realLess.implies_le with below
  have width : (X + H) - X < D by linarith
  have restricted := ContinuousOn.subinterval with continuous, weakLeft, yLeB
  obtain ⟨K, realK, integral⟩ := ContinuousOn.integrable_positive with above, restricted
  have average := ContinuousOn.right_integral_average with
    continuous, inside, control, above, yLeB, width, integral
  have position : X + H = X + H by rfl
  have secant := integralFrom.secant_right with ordered, continuous, left, above, yLeB, position, integral
  rwa ← secant at average

-- FTCFirst: the integral function of a continuous integrand has derivative
-- f(X) at every interior point. Given E, continuity controls f within E/2 on
-- a radius D around X; for steps H shorter than D and the distances to the
-- endpoints, the secant is an average of f on that stretch, so it lies within
-- E/2 of f(X).
theorem FTC.derivative_of_integral (f : Set) (A B X : Real)
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires left : A < X
  requires right : X < B
  shows HasDerivativeAt(integralFrom(f, A, B), f(X), X)
proof
  have ordered := realLess.transitive with left, right
  have weakOrdered := realLess.implies_le with ordered
  have weakLeft := realLess.implies_le with left
  have weakRight := realLess.implies_le with right
  have realX : X ∈ ℝ by typecheck
  have inside : X ∈ closedInterval(A, B)
    have data : X ∈ ℝ ∧ A ≤ X ∧ X ≤ B by refine ⟨realX, weakLeft, weakRight⟩
    exact closedInterval.membership.backward with data
  have function := integralFrom.function with weakOrdered, continuous
  have functionF : f : ℝ → ℝ
    rcases continuous with ⟨function, subset, points⟩
    exact function
  have valueFX := FunctionBetween.apply_closed with functionF
  constructor
  . exact function
    constructor
    . exact differenceQuotient.function with function
    . intros E realE positiveE
      have halfPositive := half.positive with positiveE
      obtain ⟨D, realD, positiveD, control⟩ := ContinuousOn.local_image_bounds with
        continuous, inside, halfPositive
      have positiveLeft : 0 < X - A by linarith
      have positiveRight : 0 < B - X by linarith
      obtain ⟨R, realR, positiveR, rD, rLeft, rRight⟩ := positiveMesh.common_three with
        positiveD, positiveLeft, positiveRight
      witness R
      constructor
      . exact realR
      . constructor
        . exact positiveR
        . intros H realH nonzero near
          have typedH : Real(H)
            unfold Real
            exact realH
          obtain ⟨lowerH, upperH⟩ := openBall.order_characterization.forward with near
          have bounds : f(X) - half(E) ≤ differenceQuotient(integralFrom(f, A, B), X)(H) ∧
              differenceQuotient(integralFrom(f, A, B), X)(H) ≤ f(X) + half(E)
            have sign := realLess.trichotomy at H, realZero with *
            rcases sign with negative | zero | positive
            . have above : A < X + H
                linarith
              have small : -H < D by linarith
              exact integralFrom.secant_bounds_left with
                continuous, inside, weakOrdered, weakRight, control, negative, above, small
            . exfalso
              exact nonzero with zero
            . have below : X + H < B
                linarith
              have small : H < D by linarith
              exact integralFrom.secant_bounds_right with
                continuous, inside, weakOrdered, left, control, positive, below, small
          rcases bounds with ⟨low, high⟩
          exact openBall.of_half_bounds with positiveE, low, high

-- Section: FTCContinuousDerivative
theorem CellMeanValueWitnesses.of_local_derivative (f F p : Set) (A B : Real, N : Nat)
  requires functionf : f : ℝ → ℝ
  requires continuousF : ContinuousOn(F, closedInterval(A, B))
  requires derivative : ∀ X ∈ ℝ, A < X → X < B →
    HasDerivativeAt(F, f(X), X)
  requires partition : IntervalPartition(p, A, B, N)
  shows CellMeanValueWitnesses(f, F, p, N)
proof
  intros i naturalI before
  have typedI := nat.omega.backward with naturalI
  have points : RealSequence(p)
    rcases partition with ⟨points, start, finish, steps⟩
    exact points
  have pointI := RealSequence.value at p, i with points
  have pointNext := RealSequence.value at p, succ(i) with points
  have increasing := IntervalPartition.cell with partition, before
  have onCell := ContinuousOn.partition_cell with continuousF, partition, before
  have indexLe := Less.implies_LessEqual with before
  have successorLe : succ(i) ≤ N by exact before
  have globalBounds := IntervalPartition.point_bounds with partition, indexLe
  have nextBounds := IntervalPartition.point_bounds with partition, successorLe
  have differentiable : ∀ C ∈ ℝ, (p[i]:R) < C → C < (p[succ(i)]:R) →
      ∃ D ∈ ℝ, HasDerivativeAt(F, D, C)
    intros C realC left right
    rcases globalBounds with ⟨low, high⟩
    rcases nextBounds with ⟨lowNext, highNext⟩
    have fromA : A < C by linarith
    have toB : C < B by linarith
    have derivativeAt := derivative with C, realC, fromA, toB
    have value := FunctionBetween.apply_closed with functionf, realC
    witness f(C)
    refine ⟨value, derivativeAt⟩
  obtain ⟨T, realT, left, right, D, realD, derivativeD, equation⟩ := MeanValue.theorem with
    increasing, onCell, differentiable
  have derivativeT : HasDerivativeAt(F, f(T), T)
    have boundsI := IntervalPartition.point_bounds with partition, indexLe
    have boundsNext := IntervalPartition.point_bounds with partition, successorLe
    rcases boundsI with ⟨low, high⟩
    rcases boundsNext with ⟨lowNext, highNext⟩
    have fromA : A < T by linarith
    have toB : T < B by linarith
    exact derivative with T, realT, fromA, toB
  have equal := HasDerivativeAt.unique with derivativeD, derivativeT
  have inCell : T ∈ closedInterval(p[i], p[succ(i)])
    have low := realLess.implies_le with left
    have high := realLess.implies_le with right
    have data : T ∈ ℝ ∧ p[i] ≤ T ∧ T ≤ p[succ(i)] by refine ⟨realT, low, high⟩
    exact closedInterval.membership.backward with data
  witness T
  constructor
  . exact inCell
  . unfold realMulValue
    unfold call2 at equation
    rwa equal at equation

-- FTCContinuousDerivative
theorem FTC.continuous_derivative (f : ℝ → ℝ) (F : Set) (A B : Real)
  requires ordered : A ≤ B
  requires continuousF : ContinuousOn(F, closedInterval(A, B))
  requires derivative : ∀ X ∈ ℝ, A < X → X < B →
    HasDerivativeAt(F, f(X), X)
  requires continuousf : ContinuousOn(f, closedInterval(A, B))
  shows HasRiemannIntegral(f, A, B, F(B) - F(A))
proof
  have functionf : f : ℝ → ℝ by assumption
  have functionF : F : ℝ → ℝ
    rcases continuousF with ⟨function, subset, points⟩
    exact function
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have valueA := FunctionBetween.apply_closed with functionF, realA
  have valueB := FunctionBetween.apply_closed with functionF, realB
  constructor
  . exact functionf
  . constructor
    . exact ordered
    . intros E realE positiveE
      have widthReal := realSubValue.real at B, A with *
      have scalePositive := limitScale.positive with widthReal
      have etaPositive := scaledRadius.positive with positiveE, scalePositive
      obtain ⟨D, realD, positiveD, oscillation⟩ := ContinuousOn.fine_cell_oscillation with
        continuousf, etaPositive
      witness D
      constructor
      . exact realD
      . constructor
        . exact positiveD
        . intros p t N naturalN tagged fine
          have typedN := nat.omega.backward with naturalN
          have partition : IntervalPartition(p, A, B, N)
            rcases tagged with ⟨partition, tags, cells⟩
            exact partition
          have witnesses := CellMeanValueWitnesses.of_local_derivative with
            functionf, continuousF, derivative, partition
          obtain ⟨special, equations⟩ := CellMeanValueWitnesses.tags with partition, witnesses
          have exactSum := TaggedPartition.riemann_sum_of_cell_increments with
            functionF, functionf, special, equations
          have bounds := FineCellOscillation.tagged_sum_bounds with
            functionf, oscillation, fine, tagged, special
          rw exactSum at bounds
          rcases bounds with ⟨upper, lower⟩
          have small := scaledRadius.interval_error with ordered, positiveE
          have tags : RealSequence(t)
            rcases tagged with ⟨partitionAgain, tags, cells⟩
            exact tags
          have points : RealSequence(p)
            rcases partition with ⟨points, start, finish, steps⟩
            exact points
          exact dist.lt_of_two_sided_error with upper, lower, small

-- FTCIntegrableDerivative
theorem RiemannIntegrable.continuous_derivative (f F : Set) (A B : Real)
  requires ordered : A ≤ B
  requires functionf : f : ℝ → ℝ
  requires continuousF : ContinuousOn(F, closedInterval(A, B))
  requires derivative : ∀ X ∈ ℝ, A < X → X < B →
    HasDerivativeAt(F, f(X), X)
  requires continuousf : ContinuousOn(f, closedInterval(A, B))
  shows RiemannIntegrable(f, A, B)
proof
  have functionF : F : ℝ → ℝ
    rcases continuousF with ⟨function, subset, points⟩
    exact function
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have valueA := FunctionBetween.apply_closed with functionF, realA
  have valueB := FunctionBetween.apply_closed with functionF, realB
  have typedFA : Real(F(A)) by exact valueA
  have typedFB : Real(F(B)) by exact valueB
  have endpointReal := realSubValue.real with typedFB, typedFA
  witness F(B) - F(A)
  constructor
    exact endpointReal
  . exact FTC.continuous_derivative at f, F, A, B with
      ordered, continuousF, derivative, continuousf

-- LocalDerivativeEndpoint
theorem HasRiemannIntegral.eq_endpoint_of_local_derivative (f F : Set) (A B I : Real)
  requires continuousF : ContinuousOn(F, closedInterval(A, B))
  requires derivative : ∀ X ∈ ℝ, A < X → X < B →
    HasDerivativeAt(F, f(X), X)
  requires integral : HasRiemannIntegral(f, A, B, I)
  shows I = F(B) - F(A)
proof
  have functionf : f : ℝ → ℝ
    rcases integral with ⟨function, ordered, estimates⟩
    exact function
  have functionF : F : ℝ → ℝ
    rcases continuousF with ⟨function, subset, points⟩
    exact function
  have local : ∀ p, ∀ N ∈ ℕ,
      IntervalPartition(p, A, B, N) → CellMeanValueWitnesses(f, F, p, N)
    intros p N naturalN partition
    have typedN := nat.omega.backward with naturalN
    exact CellMeanValueWitnesses.of_local_derivative with functionf, continuousF, derivative, partition
  have tags := CellMeanValueWitnesses.all_tags with local
  exact HasRiemannIntegral.eq_endpoint_of_cell_tags with functionF, integral, tags

-- Section: FundamentalTheorem
theorem FTC.identity_case (A B : Real)
  requires ordered : A ≤ B
  shows (∀ X ∈ ℝ, HasDerivativeAt(identity(ℝ), realOne, X)) ∧
    HasRiemannIntegral(constantRealFunction(realOne), A, B,
      identity(ℝ)(B) - identity(ℝ)(A))
proof
  constructor
  . intros X realX
    have typedX : Real(X) by exact realX
    exact identity.has_derivative_at with typedX
  . have integral := HasRiemannIntegral.constant at A, B, realOne with ordered
    have realA : A ∈ ℝ by simp [Real]
    have realB : B ∈ ℝ by simp [Real]
    have atA := identity.apply with realA
    have atB := identity.apply with realB
    have value : realOne * (B - A) =
        identity(ℝ)(B) - identity(ℝ)(A)
      rw [atA, atB]
      ring
    rw value at integral
    simpa [constantRealFunction] using integral

-- The constant function's derivative is zero, and the integral of zero is
-- its endpoint change.
theorem FTC.constant_case (A B C : Real)
  requires ordered : A ≤ B
  shows (∀ X ∈ ℝ, HasDerivativeAt(constantRealFunction(C), realZero, X)) ∧
    HasRiemannIntegral(constantRealFunction(realZero), A, B,
      constantRealFunction(C)(B) - constantRealFunction(C)(A))
proof
  constructor
  . intros X realX
    have typedX : Real(X) by exact realX
    exact constantRealFunction.has_derivative_at with assumption, typedX
  . have integral := HasRiemannIntegral.constant at A, B, realZero with ordered
    have valueA := constantRealFunction.value at C, A with *
    have valueB := constantRealFunction.value at C, B with *
    have value : realZero * (B - A) =
        constantRealFunction(C)(B) - constantRealFunction(C)(A)
      rw [valueA, valueB]
      ring
    rw value at integral
    simpa [constantRealFunction] using integral

-- Translating x by C leaves its derivative and endpoint change unchanged.
theorem FTC.translation_case (A B C : Real)
  requires ordered : A ≤ B
  shows (∀ X ∈ ℝ, HasDerivativeAt(translateBy(C), realOne, X)) ∧
    HasRiemannIntegral(constantRealFunction(realOne), A, B,
      translateBy(C)(B) - translateBy(C)(A))
proof
  constructor
  . intros X realX
    have typedX : Real(X) by exact realX
    have constant := constantRealFunction.has_derivative_at at C, X with
      assumption, typedX
    have identityDerivative := identity.has_derivative_at with typedX
    have sum := HasDerivativeAt.add with realZero.real, realOne.real, constant, identityDerivative
    have normalized : realZero + realOne = realOne by ring
    rw normalized at sum
    simpa [translateBy] using sum
  . have integral := HasRiemannIntegral.constant at A, B, realOne with ordered
    have atA := translateBy.value at C, A with *
    have atB := translateBy.value at C, B with *
    have value : realOne * (B - A) =
        translateBy(C)(B) - translateBy(C)(A)
      rw [atA, atB]
      ring
    rw value at integral
    simpa [constantRealFunction] using integral

-- Section: FTCExamples
theorem FTC.identity_integrand (A B X : Real)
  requires left : A < X
  requires right : X < B
  shows HasDerivativeAt(integralFrom(identity(ℝ), A, B), X, X)
proof
  have continuous := closedInterval.identity_continuous at A, B with
    *{2}
  have derivative := FTC.derivative_of_integral with continuous, left, right
  have realX : X ∈ ℝ by simp [Real]
  have value := identity.apply with realX
  rwa value at derivative

-- FTC-2: the integral of one is the endpoint change of the identity.
-- The result is an equality of real values; the earlier statements are
-- relations.
theorem FTC.integral_one (A B : Real)
  requires ordered : A ≤ B
  shows riemannIntegral(constantRealFunction(realOne), A, B) = B - A
proof
  have identityContinuous := closedInterval.identity_continuous at A, B with
    *{2}
  have constantContinuous := constantRealFunction.continuous with realOne.real
  have subset := closedInterval.subset_reals at A, B with *
  have onInterval := Continuous.continuous_on with constantContinuous, subset
  have function := Continuous.function with constantContinuous
  have derivative : ∀ X ∈ ℝ, A < X → X < B →
      HasDerivativeAt(identity(ℝ), constantRealFunction(realOne)(X), X)
    intros X realX left right
    have typedX : Real(X) by exact realX
    have atX := identity.has_derivative_at with typedX
    have value := constantRealFunction.value with realOne.real, typedX
    rwa ← value at atX
  have integral := FTC.continuous_derivative with
    ordered, identityContinuous, derivative, onInterval
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have valueA := identity.apply with realA
  have valueB := identity.apply with realB
  rw [valueA, valueB] at integral
  exact riemannIntegral.eq_of_integral with integral

-- The value form of FTC-2 is the interface most applications need.
theorem riemannIntegral.of_continuous_derivative (f F : Set) (A B : Real)
  requires ordered : A ≤ B
  requires functionf : f : ℝ → ℝ
  requires continuousF : ContinuousOn(F, closedInterval(A, B))
  requires derivative : ∀ X ∈ ℝ, A < X → X < B →
    HasDerivativeAt(F, f(X), X)
  requires continuousf : ContinuousOn(f, closedInterval(A, B))
  shows riemannIntegral(f, A, B) = F(B) - F(A)
proof
  have integral := FTC.continuous_derivative with
    ordered, continuousF, derivative, continuousf
  have functionF : F : ℝ → ℝ
    rcases continuousF with ⟨function, subset, points⟩
    exact function
  have realA : A ∈ ℝ by simp [Real]
  have realB : B ∈ ℝ by simp [Real]
  have valueA := FunctionBetween.apply_closed with functionF, realA
  have valueB := FunctionBetween.apply_closed with functionF, realB
  exact riemannIntegral.eq_of_integral with integral

-- The constant case can be used without opening the Riemann-sum layer.
theorem riemannIntegral.constant (A B L : Real)
  requires ordered : A ≤ B
  shows riemannIntegral(constantRealFunction(L), A, B) = L * (B - A)
proof
  have integral := HasRiemannIntegral.constant at A, B, L with ordered
  have normalized : HasRiemannIntegral(constantRealFunction(L), A, B, L * (B - A))
    simpa [constantRealFunction] using integral
  exact riemannIntegral.eq_of_integral with normalized