SourcePhysicalGoodResidual.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

At a good physical reference point the original top-masked residual blocks have a polynomial square bound, with the mask normalization proved from the actual hierarchy weights.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_good_reference_residual_square line 22

Source documentation

The actual good reference event discharges the error/main envelopes; the exponent is fixed independently of the later mass cutoff.

theorem physical_good_reference_residual_square {τ : Type*}
    (horder : 6 ≤ P.order) (t a : ℝ)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (hb : ∀ j l k, Measurable (b j l k))
    (hb1 : ∀ j l k u, ‖b j l k u‖ ≤ 1)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (hf : Measurable f) (hf1 : ∀ z, ‖f z‖ ≤ 1)
    (grid : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ) (cutoff : ℝ)
    (T : τ → SlopeBox) (L A D q r s : ℝ)
    (hL : 6 ≤ L) (hD : 0 ≤ D) (hdegree : D ≤ ((2*⌈L⌉₊:ℕ):ℝ))
    (hq : 0 ≤ q) (hr : 0 ≤ r) (hAb : P.absoluteConstant ≤ L^q)
    (hp : ∀ top ∈ tops, 0 ≤ precision top)
    {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SlopeBox