-- Real analysis: IndefiniteIntegral
-- 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.IndefiniteIntegral
import PartitionSplit
import RiemannSums
import ContinuousIntegral
import IntegralOrderBound

-- Section: IndefiniteIntegral
theorem FinePartition.split_at_vertex (f p t : Set) (A B C D : Real, M i : Nat)
  requires function : f : ℝ → ℝ
  requires fine : FinePartition(p, A, B, M, D)
  requires tagged : TaggedPartition(p, t, A, B, M)
  requires bounded : i ≤ M
  requires vertex : p[i] = C
  shows ∃ j ∈ ℕ, add(i, j) = M ∧
    FinePartition(p, A, C, i, D) ∧
    FinePartition(shiftedRealSequence(p, i), C, B, j, D) ∧
    TaggedPartition(p, t, A, C, i) ∧
    TaggedPartition(shiftedRealSequence(p, i), shiftedRealSequence(t, i), C, B, j) ∧
    riemannSum(f, p, t, M) =
      (riemannSum(f, p, t, i):R) +
      (riemannSum(f, shiftedRealSequence(p, i), shiftedRealSequence(t, i), j):R)
proof
  obtain ⟨j, naturalJ, sum⟩ := bounded
  have memberJ := nat.omega.forward with naturalJ
  have splitFine : FinePartition(p, A, B, add(i, j), D) by rwa sum
  have splitTagged : TaggedPartition(p, t, A, B, add(i, j)) by rwa sum
  have parts := FinePartition.split_tagged_sum with function, splitFine, splitTagged
  rw [vertex, sum] at parts
  witness j
  refine ⟨memberJ, sum, parts⟩

-- CommonMesh
theorem positiveMesh.common_two (D E : Real)
  requires positiveD : 0 < D
  requires positiveE : 0 < E
  shows ∃ H ∈ ℝ, 0 < H ∧ H ≤ D ∧ H ≤ E
proof
  have alternatives : D ≤ E ∨ ¬(D ≤ E) by tauto
  cases alternatives with first | second
  . witness D
    have realD : D ∈ ℝ by simp [Real]
    refine ⟨realD, positiveD, realLe.reflexive at D with assumption, first⟩
  . have reverse := realLess.of_not_le with second
    have weak := realLess.implies_le with reverse
    witness E
    have realE : E ∈ ℝ by simp [Real]
    refine ⟨realE, positiveE, weak, realLe.reflexive at E with assumption⟩

theorem positiveMesh.common_three (D E F : Real)
  requires positiveD : 0 < D
  requires positiveE : 0 < E
  requires positiveF : 0 < F
  shows ∃ H ∈ ℝ, 0 < H ∧ H ≤ D ∧ H ≤ E ∧ H ≤ F
proof
  obtain ⟨G, realG, positiveG, gD, gE⟩ := positiveMesh.common_two with positiveD, positiveE
  obtain ⟨H, realH, positiveH, hG, hF⟩ := positiveMesh.common_two with positiveG, positiveF
  have hD := realLe.transitive with hG, gD
  have hE := realLe.transitive with hG, gE
  witness H
  refine ⟨realH, positiveH, hD, hE, hF⟩

-- IntegralAdditivity
theorem HasRiemannIntegral.add_interior (f : Set) (A C B IL IR : Real)
  requires left : A < C
  requires right : C < B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires integralL : HasRiemannIntegral(f, A, C, IL)
  requires integralR : HasRiemannIntegral(f, C, B, IR)
  shows HasRiemannIntegral(f, A, B, IL + IR)
proof
  have function : f : ℝ → ℝ
    rcases continuous with ⟨function, subset, points⟩
    exact function
  have ordered := realLess.transitive with left, right
  rcases integralL with ⟨functionL, orderL, controlL⟩
  rcases integralR with ⟨functionR, orderR, controlR⟩
  constructor
  . exact function
  . constructor
    . exact realLess.implies_le with ordered
    . intros E realE positiveE
      have typedE : Real(E) by exact realE
      have halfReal := half.real with typedE
      have halfPositive := half.positive with positiveE
      have quarterReal := half.real with halfReal
      have quarterPositive := half.positive with halfPositive
      obtain ⟨DC, realDC, positiveDC, compare⟩ := ContinuousOn.fine_sums_close with
        ordered, continuous, halfPositive
      obtain ⟨DL, realDL, positiveDL, estimateL⟩ :=
        controlL with half(half(E)), quarterPositive
      obtain ⟨DR, realDR, positiveDR, estimateR⟩ :=
        controlR with half(half(E)), quarterPositive
      obtain ⟨D, realD, positiveD, dC, dL, dR⟩ := positiveMesh.common_three with
        positiveDC, positiveDL, positiveDR
      witness D
      constructor
      . exact realD
      . constructor
        . exact positiveD
        . intros p t N naturalN tagged fine
          have typedN := nat.omega.backward with naturalN
          obtain ⟨q, M, naturalM, u, v, fineQ, taggedQ, shared, preserved, i, naturalI, boundedI, vertex⟩ := FinePartition.insert_or_hit with
            function, fine, left, right
          have typedM := nat.omega.backward with naturalM
          have typedI := nat.omega.backward with naturalI
          have finePCompare := FinePartition.weaken with fine, dC
          have fineQCompare := FinePartition.weaken with fineQ, dC
          have nearPQ := compare with p, t, N, naturalN, q, leftPartitionTags(q), M,
            naturalM, tagged, finePCompare, taggedQ, fineQCompare
          obtain ⟨j, naturalJ, sumIndex, finePrefix, fineSuffix, taggedPrefix, taggedSuffix, splitSum⟩ := FinePartition.split_at_vertex with
            function, fineQ, taggedQ, boundedI, vertex
          have typedJ := nat.omega.backward with naturalJ
          have fineLocalL := FinePartition.weaken with finePrefix, dL
          have fineLocalR := FinePartition.weaken with fineSuffix, dR
          have nearL := estimateL with q, leftPartitionTags(q), i, naturalI,
            taggedPrefix, fineLocalL
          have nearR := estimateR with shiftedRealSequence(q, i),
            shiftedRealSequence(leftPartitionTags(q), i), j, naturalJ,
            taggedSuffix, fineLocalR
          have pointsQ : RealSequence(q)
            rcases taggedQ with ⟨partition, tags, cells⟩
            rcases partition with ⟨points, start, finish, increasing⟩
            exact points
          have tagsQ : RealSequence(leftPartitionTags(q))
            rcases taggedQ with ⟨partition, tags, cells⟩
            exact tags
          have pointsR := shiftedRealSequence.sequence at q, i with pointsQ
          have tagsR := shiftedRealSequence.sequence at leftPartitionTags(q), i with tagsQ
          have sumL := riemannSum.real at f, q, leftPartitionTags(q), i with
            function, pointsQ, tagsQ
          have sumR := riemannSum.real at f, shiftedRealSequence(q, i),
            shiftedRealSequence(leftPartitionTags(q), i), j with function, pointsR, tagsR
          have memberL : riemannSum(f, q, leftPartitionTags(q), i) ∈ ℝ by exact sumL
          have memberR : riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j) ∈ ℝ
            exact sumR
          have dataL : riemannSum(f, q, leftPartitionTags(q), i) ∈ ℝ ∧ dist(riemannSum(f, q, leftPartitionTags(q), i), IL) < half(half(E))
            refine ⟨memberL, nearL⟩
          have dataR : riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j) ∈ ℝ ∧ dist(riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j), IR) < half(half(E))
            refine ⟨memberR, nearR⟩
          have ballL := openBall.membership.backward with dataL
          have ballR := openBall.membership.backward with dataR
          have ballSum := openBall.add at
            riemannSum(f, q, leftPartitionTags(q), i),
            riemannSum(f, shiftedRealSequence(q, i), shiftedRealSequence(leftPartitionTags(q), i), j),
            IL, IR, half(half(E)), half(half(E)) with
              sumL, sumR, *{2}, quarterReal, quarterReal, ballL, ballR
          have quarters := half.add_self with halfReal
          rw [quarters, ← splitSum] at ballSum
          have pointsP : RealSequence(p)
            rcases tagged with ⟨partition, tags, cells⟩
            rcases partition with ⟨points, start, finish, increasing⟩
            exact points
          have tagsP : RealSequence(t)
            rcases tagged with ⟨partition, tags, cells⟩
            exact tags
          have sumP := riemannSum.real at f, p, t, N with function, pointsP, tagsP
          have memberP : riemannSum(f, p, t, N) ∈ ℝ by exact sumP
          have dataPQ : riemannSum(f, p, t, N) ∈ ℝ ∧ dist(riemannSum(f, p, t, N), riemannSum(f, q, leftPartitionTags(q), M)) < half(E)
            refine ⟨memberP, nearPQ⟩
          have ballPQ := openBall.membership.backward with dataPQ
          have together := openBall.triangle with ballPQ, ballSum
          have halves := half.add_self with typedE
          rw halves at together
          obtain ⟨realSum, bound⟩ := openBall.membership.forward with together
          exact bound

-- LocalContinuity
theorem ContinuousWithinAt.mono (f S T : Set) (A : Real)
  requires continuous : ContinuousWithinAt(f, T, A)
  requires subset : S ⊆ T
  shows ContinuousWithinAt(f, S, A)
proof
  rcases continuous with ⟨function, reals, control⟩
  constructor
  . exact function
  . constructor
      intros X member
      have included : X ∈ T by exact subset with X, member
      exact reals with X, included
    . intros E realE positive
      obtain ⟨D, realD, positiveD, maps⟩ := control with E, realE, positive
      witness D
      constructor
      . exact realD
      . constructor
        . exact positiveD
        . intros X realX member near
          have included : X ∈ T by exact subset with X, member
          exact maps with X, realX, included, near

theorem ContinuousOn.mono (f S T : Set)
  requires continuous : ContinuousOn(f, T)
  requires subset : S ⊆ T
  shows ContinuousOn(f, S)
proof
  rcases continuous with ⟨function, reals, atPoints⟩
  constructor
  . exact function
  . constructor
      intros X member
      have included : X ∈ T by exact subset with X, member
      exact reals with X, included
    . intros X member
      have included : X ∈ T by exact subset with X, member
      have point := atPoints with X, included
      have typedX : Real(X)
        unfold Real
        exact reals with X, included
      exact ContinuousWithinAt.mono with point, subset

theorem ContinuousOn.partition_cell (F p : Set) (A B : Real, N i : Nat)
  requires continuous : ContinuousOn(F, closedInterval(A, B))
  requires partition : IntervalPartition(p, A, B, N)
  requires before : i < N
  shows ContinuousOn(F, closedInterval(p[i], p[succ(i)]))
proof
  have subset := IntervalPartition.cell_subset with partition, before
  exact ContinuousOn.mono with continuous, subset

-- IndefiniteIntegral
theorem ContinuousOn.subinterval (f : Set) (A B X Y : Real)
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires left : A ≤ X
  requires right : Y ≤ B
  shows ContinuousOn(f, closedInterval(X, Y))
proof
  have subset := closedInterval.nested with left, right
  exact ContinuousOn.mono with continuous, subset

defunique integralValue (f : Set, A B X : Real) (I ∈ ℝ) :=
  (X ∈ closedInterval(A, B) → HasRiemannIntegral(f, A, X, I)) ∧
  (¬(X ∈ closedInterval(A, B)) → I = realZero)
requires ordered : A ≤ B
requires continuous : ContinuousOn(f, closedInterval(A, B))
proof
  have alternatives : X ∈ closedInterval(A, B) ∨ ¬(X ∈ closedInterval(A, B)) by tauto
  cases alternatives with inside | outside
  . have bounds := closedInterval.membership.forward at A, B, X with inside
    rcases bounds with ⟨realX, lower, upper⟩
    have restricted := ContinuousOn.subinterval at f, A, B, A, X with
      continuous, realLe.reflexive at A with assumption, upper
    obtain ⟨I, realI, integral⟩ := ContinuousOn.integrable_interval with lower, restricted
    witness I
    constructor
    . exact realI
    . constructor
      . intro again
        exact integral
      . intro impossible
        exfalso
        exact impossible with inside
  . witness realZero
    constructor
    . have realZ := realZero.real
      exact realZ
    . constructor
      . intro impossible
        exfalso
        exact outside with impossible
      . intro ignored
        rfl

uniqueness
  intros I memberI first J memberJ second
  have alternatives : X ∈ closedInterval(A, B) ∨ ¬(X ∈ closedInterval(A, B)) by tauto
  cases alternatives with inside | outside
  . have firstIntegral : HasRiemannIntegral(f, A, X, I)
      tauto
    have secondIntegral : HasRiemannIntegral(f, A, X, J) by tauto
    obtain ⟨typedX, lower, upper⟩ := closedInterval.membership.forward with inside
    exact HasRiemannIntegral.unique_on_interval with *
  . have firstZero : I = realZero
      tauto
    have secondZero : J = realZero by tauto
    cc

defgraph integralFrom (f : Set, A B : Real) (X ∈ ℝ) : ℝ := integralValue(f, A, B, X)
requires ordered : A ≤ B
requires continuous : ContinuousOn(f, closedInterval(A, B))
proof
  obtain ⟨realValue, inside, outside⟩ := integralValue.selected at f, A, B, X with ordered, continuous
  exact realValue

theorem integralFrom.integral (f : Set) (A B X : Real)
  requires ordered : A ≤ B
  requires continuous : ContinuousOn(f, closedInterval(A, B))
  requires inside : X ∈ closedInterval(A, B)
  shows HasRiemannIntegral(f, A, X, integralFrom(f, A, B)(X))
proof
  obtain ⟨realValue, valid, outside⟩ := integralValue.selected at f, A, B, X with ordered, continuous
  have integral := valid with inside
  have value := integralFrom.value at f, A, B, X with ordered, continuous
  rwa value

theorem integralFrom.increment_right (f : Set) (A B X Y 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 local : HasRiemannIntegral(f, X, Y, I)
  shows integralFrom(f, A, B)(Y) =
    integralFrom(f, A, B)(X) + I
proof
  have weakLeft := realLess.implies_le with left
  have weakMiddle := realLess.implies_le with middle
  have xBound : X ≤ B by exact realLe.transitive at X, Y, B with weakMiddle, right
  have realX : X ∈ ℝ by simp [Real]
  have realY : Y ∈ ℝ by simp [Real]
  have insideX : X ∈ closedInterval(A, B)
    have data : X ∈ ℝ ∧ A ≤ X ∧ X ≤ B by refine ⟨realX, weakLeft, xBound⟩
    exact closedInterval.membership.backward with data
  have insideY : Y ∈ closedInterval(A, B)
    have weakAY := realLe.transitive with weakLeft, weakMiddle
    have data : Y ∈ ℝ ∧ A ≤ Y ∧ Y ≤ B by refine ⟨realY, weakAY, right⟩
    exact closedInterval.membership.backward with data
  have first := integralFrom.integral with ordered, continuous, insideX
  have whole := integralFrom.integral with ordered, continuous, insideY
  have restricted := ContinuousOn.subinterval at f, A, B, A, Y with
    continuous, realLe.reflexive at A with assumption, right
  have combined := HasRiemannIntegral.add_interior with left, middle, restricted, first, local
  have strict := realLess.transitive with left, middle
  exact HasRiemannIntegral.unique_positive with strict, whole, combined

theorem integralFrom.increment_left (f : Set) (A B X Y 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 local : HasRiemannIntegral(f, Y, X, I)
  shows integralFrom(f, A, B)(X) =
    integralFrom(f, A, B)(Y) + I
proof
  exact integralFrom.increment_right with ordered, continuous, left, middle, right, local