-- Real analysis: Examples
-- 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.Examples
import Sequences
import Power
import Differentiation
import SequentialCompactness

-- Section: Powers
def powSequence (u : Set, k : Nat) → Set
  | u, zero => constantSequence(realOne)
  | u, succ(k) => mulSequence(u, powSequence(u, k))

theorem powSequence.sequence (u : Set, k : Nat)
  requires sequence : RealSequence(u)
  shows RealSequence(powSequence(u, k))
proof
  induction k
  | zero =>
    rw powSequence
    exact constantSequence.sequence with realOne.real
  | succ(j) using ih =>
    rw powSequence
    exact mulSequence.sequence with sequence, ih

theorem powSequence.value (u : Set, k n : Nat)
  requires sequence : RealSequence(u)
  shows powSequence(u, k)[n] = uₙ ^ k
proof
  induction k
  | zero =>
    have constantValue := constantSequence.value at realOne, n with
      realOne.real, assumption
    rw powSequence
    rw constantValue
    rw realPow.zero
    rfl
  | succ(j) using ih =>
    have valueReal := RealSequence.value at u, n with sequence
    have powerSequence := powSequence.sequence at u, j with sequence
    have powerValueReal := RealSequence.value at powSequence(u, j), n with
      powerSequence
    have productValue := mulSequence.value at
      u, powSequence(u, j), n with
        sequence, powerSequence, valueReal, powerValueReal
    rw powSequence
    rw productValue
    rw ih
    rw realPow.succ
    rfl

theorem ConvergesTo.pow (u : Set) (L : Real, k : Nat)
  requires converges : ConvergesTo(u, L)
  shows ConvergesTo(powSequence(u, k), L ^ k)
proof
  induction k
  | zero =>
    rw powSequence
    rw realPow.zero
    exact constantSequence.converges with realOne.real
  | succ(j) using ih =>
    rw powSequence
    rw realPow.succ
    exact ConvergesTo.mul at u, powSequence(u, j), L, L ^ j with
      converges, ih

-- Section: Examples
theorem constantSequence.quotient_converges (A B : Real)
  requires nonzero : B ≠ 0
  shows ConvergesTo(
    divSequence(constantSequence(A), constantSequence(B)), A / B)
proof
  exact ConvergesTo.div at
    constantSequence(A), constantSequence(B), A, B with
      constantSequence.converges at A with assumption,
      constantSequence.converges at B with assumption,
      nonzero

-- In particular, the constant reciprocal sequence converges to 1/L.
theorem constantSequence.reciprocal_converges (L : Real)
  requires nonzero : L ≠ 0
  shows ConvergesTo(
    divSequence(constantSequence(1), constantSequence(L)), 1 / L)
proof
  exact constantSequence.quotient_converges with realOne.real, nonzero

-- Negation preserves every convergent sequence because it is continuous.
theorem convergentSequence.negation_example (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  shows ConvergesTo(compose(realNeg, u, ℕ, ℝ, ℝ), -L)
proof
  have mapped := ContinuousAt.converges at realNeg, u, L with
    realNeg.continuous_at at L with assumption, converges
  exact mapped

-- The square function is continuous because it is the pointwise product of
-- the identity function with itself.
theorem squareFunction.continuous
  shows Continuous(pointwiseMul(identity(ℝ), identity(ℝ)))
proof
  exact Continuous.mul with identity.continuous, identity.continuous

-- The reciprocal function is continuous at every nonzero real.
theorem reciprocalFunction.continuous_at (A : Real)
  requires nonzero : A ≠ 0
  shows ContinuousAt(pointwiseInv(identity(ℝ)), A)
proof
  have realA : A ∈ ℝ by simp [Real]
  have mappedA := identity.relates with realA
  have identityValue := FunctionBetween.apply_value at
    identity(ℝ), ℝ, ℝ, A, A with
      identity.function at ℝ, realA, mappedA
  have identityNonzero : Nonzero(identity(ℝ)(A))
    unfold Nonzero
    rwa identityValue
  exact ContinuousAt.inv at identity(ℝ), A with
    identity.continuous_at at A with assumption, identityNonzero

-- Closed intervals are preserved by limits.  This first concrete order-limit
-- example says that a convergent sequence contained in [0, 1] has its limit
-- in the same interval.
theorem convergentSequence.unit_interval_limit (u : Set) (L : Real)
  requires converges : ConvergesTo(u, L)
  requires contained : UnitIntervalTerms(u)
  shows 0 ≤ L ∧ L ≤ 1
proof
  have lower : NonnegativeTerms(u)
    intros n nNatural
    obtain ⟨lower, upper⟩ := contained with n, nNatural
    exact lower
  have upper : BoundedAboveBy(u, realOne)
    intros n nNatural
    have bounds := contained with n, nNatural
    rcases bounds with ⟨lower, upper⟩
    exact upper
  constructor
  . exact ConvergesTo.nonnegative_of_nonnegative_terms at
      u, L with converges, lower
  . exact ConvergesTo.le_constant at u, L, realOne with
      realOne.real, converges, upper

-- Natural powers preserve limits, with handwritten notation for
-- both the sequence terms and their limit.
theorem convergentSequence.power_example (u : Set) (L : Real, k : Nat)
  requires converges : ConvergesTo(u, L)
  shows ConvergesTo(powSequence(u, k), L ^ k)
proof
  exact ConvergesTo.pow with converges

-- Completeness gives a canonical limit to every bounded nondecreasing real
-- sequence: the supremum of its range.
theorem boundedNondecreasingSequence.converges (u : Set) (B : Real)
  requires sequence : RealSequence(u)
  requires increasing : Nondecreasing(u)
  requires bounded : BoundedAboveBy(u, B)
  shows ConvergesTo(u, realSup(range(u)))
proof
  exact Nondecreasing.converges_to_supremum with sequence, increasing, bounded

-- The identity function tends to A as x tends to A through the punctured
-- neighborhood used by the derivative definition.
theorem identityFunction.limit_example (A : Real)
  shows TendsToAt(identity(ℝ), A, A)
proof
  exact identity.tends_to_at with assumption

-- A strict comparison at one point persists throughout a neighborhood.
theorem continuousFunctions.order_persists (f g : Set) (A : Real)
  requires continuousF : ContinuousAt(f, A)
  requires continuousG : ContinuousAt(g, A)
  requires below : Below(f(A), g(A))
  shows ∃ D ∈ ℝ, 0 < D ∧
    ∀ x ∈ ℝ, (x ∈ openBall(A, D) → Below(f(x), g(x)))
proof
  exact ContinuousAt.eventually_lt with continuousF, continuousG, below

-- The difference quotient of a constant function tends to zero.
theorem derivative.constant_example (C A : Real)
  shows HasDerivativeAt(constantRealFunction(C), realZero, A)
proof
  exact constantRealFunction.has_derivative_at with *{2}

-- The difference quotient of x ↦ x tends to one at every point.
theorem derivative.identity_example (A : Real)
  shows HasDerivativeAt(identity(ℝ), realOne, A)
proof
  exact identity.has_derivative_at with assumption

-- Linearity combines checked derivatives as on paper.
theorem derivative.doubled_identity (A : Real)
  shows HasDerivativeAt(
    pointwiseAdd(identity(ℝ), identity(ℝ)), (2:R), A)
proof
  have doubled := HasDerivativeAt.add at
    identity(ℝ), identity(ℝ), realOne, realOne, A with
      identity.has_derivative_at at A with assumption,
      identity.has_derivative_at at A with assumption
  have two : (1:R) + 1 = (2:R) by ring
  rw two at doubled
  exact doubled

-- Differentiability immediately supplies the continuity needed by later
-- analysis arguments.
theorem derivative.identity_is_continuous (A : Real)
  shows ContinuousAt(identity(ℝ), A)
proof
  exact HasDerivativeAt.continuous_at at
    identity(ℝ), realOne, A with
      identity.has_derivative_at at A with assumption

-- The product rule gives (x²)'(A) = A + A.
theorem derivative.square (A : Real)
  shows HasDerivativeAt(
    pointwiseMul(identity(ℝ), identity(ℝ)), A + A, A)
proof
  have derivative := HasDerivativeAt.mul at
    identity(ℝ), identity(ℝ), realOne, realOne, A with
      identity.has_derivative_at at A with assumption,
      identity.has_derivative_at with assumption
  have realA : A ∈ ℝ by simp [Real]
  have mapped := identity.relates with realA
  have value := FunctionBetween.apply_value at
    identity(ℝ), ℝ, ℝ, A, A with
      identity.function at ℝ, realA, mapped
  unfold realAddValue at derivative
  unfold realMulValue at derivative
  rw value at derivative
  have oneLeft := realMulValue.one_left at A
  have oneRight := realMulValue.one_right at A
  unfold call2 at oneLeft
  unfold call2 at oneRight
  rw [oneLeft, oneRight] at derivative
  unfold call2
  exact derivative