SourcePhysicalResidualNorm.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original physical residual at one angular block has a uniform polynomial norm bound. This controls the one possible long-packet block; no total label count or carrier-frequency factor enters.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalMaskedValue_eq_complex_cross line 22

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physical_masked_residual_norm line 44

Source documentation

Absolute summation at each source length, followed by the exact mask/mass coefficient estimate, controls any single residual block.

theorem physical_masked_residual_norm {τ : Type*}
    (horder : 6 ≤ P.order) (t : ℝ) (d radius : Fin N → ℝ) (M : ℝ) (K H : ℕ)
    (hd : ∀ j, 0 < d j) (hM : 0 ≤ M) (hradius : ∀ j, radius j ≤ K)
    (hlocal : ∀ j, SourceSlopeLabels.LocalMultiplicity Finset.univ
      (fun l : P.labels j => t+P.rowSlope j l) (d j) H)
    (b : ∀ j, P.labels j → κ → ℝ → ℂ) (hb : ∀ j l k, Measurable (b j l k))
    (hbM : ∀ j l k s, ‖b j l k s‖ ≤ M)
    (hsupport : ∀ j l k s, b j l k s ≠ 0 →
      |s-(t+P.rowSlope j l)| ≤ radius j*d j)
    (v : ℝ×ℝ → ℝ) (hv : Measurable v)
    (f : ℝ×ℝ → EuclideanSpace ℂ κ) (hf : Measurable f) (hf1 : ∀ z, ‖f z‖ ≤ 1)
    (grid : AngularGrid) (tops : Finset τ) (slope precision : τ → ℝ) (cutoff : ℝ)
…

Mentions: OAI.LipschitzHilbert.SourceSlopeLabels.LocalMultiplicity, OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_physical_shifted_residual_norm line 99

Source documentation

Source stopping and the rounded block length absorb every constant in the physical single-block estimate before a family is chosen.

theorem eventually_physical_shifted_residual_norm
    (q D M : ℝ) (hD : 0 ≤ D) (hM : 0 ≤ M) (K H : ℕ) :
    ∀ᶠ 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 : ℝ) (d radius : Fin N → ℝ), (∀ j, 0 < d j) → (∀ j, radius j ≤ K) →
      (∀ j, SourceSlopeLabels.LocalMultiplicity Finset.univ
        (fun l : P.labels j => t+P.rowSlope j l) (d j) H) →
    ∀ (b : ∀ j, P.labels j → κ → ℝ → ℂ),
…

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