IndisputableMonolith.Cost.ClassicalResults

   1import Mathlib
   2
   3/-!
   4# Classical Mathematical Results
   5
   6HEADER CORRECTED (2026-07-06): an earlier revision of this module declared
   7these results as `axiom`s; every one has since been PROVED as a `theorem`
   8over Mathlib (the body below contains no `axiom` declarations). The stale
   9header claiming otherwise confused auditors and is replaced by this note.
  10
  11These are standard mathematical facts from real analysis, complex analysis,
  12and functional equations, now formalized.
  13
  14## References
  15
  161. Aczél, J. (1966). *Lectures on Functional Equations and Their Applications*. Academic Press.
  172. Kuczma, M. (2009). *An Introduction to the Theory of Functional Equations and Inequalities*. Birkhäuser.
  183. Ahlfors, L. V. (1979). *Complex Analysis* (3rd ed.). McGraw-Hill.
  194. Conway, J. B. (1978). *Functions of One Complex Variable*. Springer.
  205. Apostol, T. M. (1974). *Mathematical Analysis* (2nd ed.). Addison-Wesley.
  216. Rudin, W. (1976). *Principles of Mathematical Analysis* (3rd ed.). McGraw-Hill.
  22
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Cost
  27namespace ClassicalResults
  28
  29open Real Complex
  30
  31/-! ## Provable Classical Results -/
  32
  33private lemma spherical_cap_pos (θmin : ℝ) (hθ : θmin ∈ Set.Icc (0 : ℝ) (Real.pi/2)) :
  34    0 ≤ (2 * Real.pi * (1 - Real.cos θmin)) := by
  35  have h1 : Real.cos θmin ≤ 1 := Real.cos_le_one θmin
  36  have h2 : 0 ≤ 1 - Real.cos θmin := by linarith
  37  have h3 : 0 ≤ 2 * Real.pi := by positivity
  38  exact mul_nonneg h3 h2
  39
  40private lemma exp_mul_rearrange (c₁ c₂ φ₁ φ₂ : ℝ) :
  41    Complex.exp (-(c₁+c₂)/2) * Complex.exp ((φ₁+φ₂) * I) =
  42    (Complex.exp (-c₁/2) * Complex.exp (φ₁ * I)) * (Complex.exp (-c₂/2) * Complex.exp (φ₂ * I)) := by
  43  rw [← Complex.exp_add, ← Complex.exp_add, ← Complex.exp_add, ← Complex.exp_add]
  44  congr 1
  45  push_cast
  46  ring
  47
  48/-- Provable version with integrability hypotheses -/
  49theorem piecewise_path_integral_additive_integrable (f : ℝ → ℝ) (a b c : ℝ)
  50    (hab : IntervalIntegrable f MeasureTheory.volume a b)
  51    (hbc : IntervalIntegrable f MeasureTheory.volume b c) :
  52    ∫ x in a..c, f x = (∫ x in a..b, f x) + (∫ x in b..c, f x) :=
  53  (intervalIntegral.integral_add_adjacent_intervals hab hbc).symm
  54
  55/-! ## Real/Complex Hyperbolic Functions -/
  56
  57theorem real_cosh_exponential_expansion (t : ℝ) :
  58    ((Real.exp t + Real.exp (-t)) / 2) = Real.cosh t := by
  59  simpa using (Real.cosh_eq t).symm
  60
  61/-! ## Complex Exponential Norms -/
  62
  63theorem complex_norm_exp_ofReal (r : ℝ) : ‖Complex.exp r‖ = Real.exp r := by
  64  rw [Complex.norm_exp]
  65  simp [Complex.ofReal_re]
  66
  67theorem complex_norm_exp_I_mul (θ : ℝ) : ‖Complex.exp (θ * I)‖ = 1 := by
  68  simpa using Complex.norm_exp_ofReal_mul_I θ
  69
  70/-! ## Trigonometric/logarithmic limits and monotonic consequences -/
  71
  72theorem neg_log_sin_tendsto_atTop_at_zero_right :
  73    Filter.Tendsto (fun θ => - Real.log (Real.sin θ)) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by
  74  -- sin(θ) → 0⁺ as θ → 0⁺, so log(sin(θ)) → -∞, so -log(sin(θ)) → +∞
  75  -- Use: f → -∞ implies -f → +∞
  76  rw [← Filter.tendsto_neg_atBot_iff]
  77  simp only [neg_neg]
  78  -- Now need: log(sin θ) → -∞ as θ → 0⁺
  79
  80  -- sin θ → 0 as θ → 0 (from continuity)
  81  have h_sin_tends_zero : Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) := by
  82    have h_cont : Continuous Real.sin := Real.continuous_sin
  83    simpa [Real.sin_zero] using h_cont.tendsto 0 |>.mono_left nhdsWithin_le_nhds
  84
  85  -- sin θ > 0 near 0⁺ (eventually)
  86  have h_sin_pos : ∀ᶠ θ in nhdsWithin 0 (Set.Ioi 0), 0 < Real.sin θ := by
  87    have h_Iio_pi : Set.Iio Real.pi ∈ nhds (0 : ℝ) := Iio_mem_nhds Real.pi_pos
  88    filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds h_Iio_pi] with θ hθ_pos hθ_lt_pi
  89    exact Real.sin_pos_of_pos_of_lt_pi hθ_pos hθ_lt_pi
  90
  91  -- Combine: sin θ → 0⁺ as θ → 0⁺
  92  have h_sin_tends_zero_pos :
  93      Filter.Tendsto Real.sin (nhdsWithin 0 (Set.Ioi 0)) (nhdsWithin 0 (Set.Ioi 0)) := by
  94    rw [tendsto_nhdsWithin_iff]
  95    exact ⟨h_sin_tends_zero, h_sin_pos⟩
  96
  97  -- log x → -∞ as x → 0⁺
  98  have h_log_atBot := Real.tendsto_log_nhdsGT_zero
  99
 100  -- Compose
 101  exact h_log_atBot.comp h_sin_tends_zero_pos
 102
 103theorem theta_min_spec_inequality :
 104    ∀ (Amax θ : ℝ), 0 < Amax → 0 < θ → θ ≤ π/2 →
 105      (- Real.log (Real.sin θ) ≤ Amax) →
 106      θ ≥ Real.arcsin (Real.exp (-Amax)) := by
 107  intro Amax θ _hAmax hθpos hθle hlog
 108  have h1 : Real.log (Real.sin θ) ≥ -Amax := by linarith
 109  have hsin_pos : 0 < Real.sin θ := Real.sin_pos_of_pos_of_lt_pi hθpos (by linarith [Real.pi_pos])
 110  have h2 : Real.sin θ ≥ Real.exp (-Amax) := by
 111    have := Real.exp_log hsin_pos
 112    rw [← this]
 113    exact Real.exp_le_exp.mpr h1
 114  have h3 : Real.arcsin (Real.sin θ) = θ := by
 115    apply Real.arcsin_sin
 116    · linarith
 117    · linarith [Real.pi_pos]
 118  rw [← h3]
 119  exact Real.arcsin_le_arcsin h2
 120
 121theorem theta_min_range :
 122    ∀ Amax > 0,
 123      0 < Real.arcsin (Real.exp (-Amax)) ∧ Real.arcsin (Real.exp (-Amax)) ≤ π/2 := by
 124  intro Amax hAmax
 125  constructor
 126  · rw [Real.arcsin_pos]
 127    exact Real.exp_pos _
 128  · exact Real.arcsin_le_pi_div_two _
 129
 130theorem spherical_cap_measure_bounds :
 131    ∀ θmin ∈ Set.Icc (0 : ℝ) (Real.pi/2),
 132      0 ≤ (2 * Real.pi * (1 - Real.cos θmin)) :=
 133  spherical_cap_pos
 134
 135/-! ## Complex Exponential Algebra -/
 136
 137theorem complex_exp_mul_rearrange :
 138    ∀ (c₁ c₂ φ₁ φ₂ : ℝ),
 139      Complex.exp (-(c₁+c₂)/2) * Complex.exp ((φ₁+φ₂) * I) =
 140      (Complex.exp (-c₁/2) * Complex.exp (φ₁ * I)) * (Complex.exp (-c₂/2) * Complex.exp (φ₂ * I)) :=
 141  exp_mul_rearrange
 142
 143/-!
 144NOTE: `continuousOn_extends_to_continuous` was removed because it is mathematically false.
 145Counterexample: `sin(1/x)` is continuous on `(0, ∞)` but has no continuous extension to `0`.
 146See `docs/FALSE_AXIOMS_ANALYSIS.md` for details.
 147-/
 148
 149end ClassicalResults
 150end Cost
 151end IndisputableMonolith
 152