SourcePhysicalShiftedResidual.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual shifted angular blocks satisfy the good-reference residual square estimate with a fixed polynomial exponent.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_physical_shifted_good_reference_residual_square line 17

Source documentation

Source dyadic stopping and the good event discharge the block count, mask normalization and positive reference envelopes simultaneously.

theorem eventually_physical_shifted_good_reference_residual_square
    (q D : ℝ) (hq : 0 ≤ q) (hD : 0 ≤ D) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (N : ℕ) (κ : Type) (Label : Fin N → Type) (Item : ∀ j, Label j → Type)
      [Fintype κ] [∀ j l, Fintype (Item j l)]
      (P : SourceLabeledLattice N κ Label Item), 6 ≤ P.order → P.absoluteConstant ≤ L^q →
    ∀ (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
      (t a : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ),
      (∀ j l k, Measurable (b j l k)) → (∀ j l k u, ‖b j l k u‖ ≤ 1) →
    ∀ (v : ℝ×ℝ → ℝ), Measurable v →
    ∀ (f : ℝ×ℝ → EuclideanSpace ℂ κ), Measurable f → (∀ z, ‖f z‖ ≤ 1) →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarProfileConstant