structure definition def or abbrev

`AlphaPrecisionHypothesis`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 170structure AlphaPrecisionHypothesis where
 171  deltas : ℕ → ℝ
 172  delta_1_matches : deltas 1 = delta_1
 173  converges_to_CODATA : Filter.Tendsto
 174    (fun N => partial_alpha alpha_seed (deltas 1) deltas N) Filter.atTop
 175    (nhds CODATA_alpha_inv)
 176
 177/-! ## Bounds on δ₂ -/
 178
 179/-- The residual between additive formula and CODATA.
 180    This is the amount the remaining δ_n terms must sum to. -/

depends on (11)

Lean names referenced from this declaration's body.

alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
CODATA_alpha_inv in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
delta_1 in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
partial_alpha in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use