def
definition
IsHighCalibratedLog
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.AlphaCoordinateFixation on GitHub at line 151.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
148
149/-- **Higher-derivative calibration**: a cost function in log coordinates
150satisfies `G^(4)(0) = 1`. -/
151def IsHighCalibratedLog (G : ℝ → ℝ) : Prop :=
152 deriv (deriv (deriv (deriv G))) 0 = 1
153
154/-- The α-cost is high-calibrated iff `α² = 1`. -/
155theorem costAlphaLog_high_calibrated_iff (α : ℝ) (hα : α ≠ 0) :
156 IsHighCalibratedLog (CostAlphaLog α) ↔ α ^ 2 = 1 := by
157 unfold IsHighCalibratedLog
158 rw [costAlphaLog_fourth_deriv_at_zero α hα]
159
160/-! ## The α-pin -/
161
162/-- **The α-pin theorem.** Within the bilinear `α`-family with the
163rigidity-paper convention `α ≥ 1`, higher-derivative calibration forces
164`α = 1`. -/
165theorem alpha_pin_under_high_calibration
166 (α : ℝ) (h_pos : 1 ≤ α)
167 (h_calib : IsHighCalibratedLog (CostAlphaLog α)) :
168 α = 1 := by
169 have hα_ne : α ≠ 0 := by linarith
170 have hα_sq : α ^ 2 = 1 :=
171 (costAlphaLog_high_calibrated_iff α hα_ne).mp h_calib
172 -- α ≥ 1 and α² = 1 forces α = 1.
173 nlinarith
174
175/-! ## J is the unique high-calibrated bilinear cost -/
176
177/-- The `α = 1` bilinear cost is exactly `Jcost`. -/
178theorem alpha_pinned_to_one_implies_J (x : ℝ) (hx : 0 < x) :
179 CostAlpha 1 x = Jcost x :=
180 cost_alpha_one_eq_jcost x hx
181
papers checked against this theorem (showing 1 of 1)
-
Finite R-transform approximates standard version within O(1/N)
"H_µ(z) = ∫ log(z − t) dµ(t); H*_µ(s) := inf_{x>0}{sx − H_µ(x)}; (H*)'(H'(x)) = x."