SourceReferenceBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Square and cubic-variation moments for the actual normalized reference collection. Its root window need only contain retained lengths, so the short-packet restriction introduces no larger window.

def OAI.LipschitzHilbert.SourceLatticePacket.referenceSquareMomentCost line 16
def OAI.LipschitzHilbert.SourceLatticePacket.referenceVariationMomentCost line 21

theorem OAI.LipschitzHilbert.SourceLatticePacket.reference_uniform_moments line 29

Source documentation

Both constants precede all finite index types and the horizontal scale. The spectra are the concrete annuli proved from original packet spectra by frozenProfile_fourier_cutoffs.

theorem reference_uniform_moments (hL : LepingleInput) {lo hi : ℝ}
    (hlo : 0 < lo) (hhi : 0 ≤ hi) :
    ∃ A M : ℝ, 0 < A ∧ 0 < M ∧ ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι)
      (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ) (hv : Measurable v)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (hg : Measurable g) (hg1 : ∀ z, ‖g z‖ ≤ 1),
      Monotone d →
      (∀ j u k y xi, |xi| < (lo/P.topLength)*(2:ℝ)^j.val → 𝓕 (P.raw 0 j u k y) xi = 0) →
      (∀ j u k y xi, (hi/P.topLength)*(2:ℝ)^j.val < |xi| → 𝓕 (P.raw 0 j u k y) xi = 0) →
      ∀ (y : ℝ) (grid : FiniteLineGrid), 1 < grid.branching →
      (∀ j (_u : ι j), P.length j ≤ P.topLength*grid.width) → ∀ p : ℝ, 0 ≤ p →
      let Q := P.referenceAnalyzedLine d v hv g hg hg1 y
…

Mentions: OAI.LipschitzHilbert.LepingleInput, OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.FiniteLineGrid

theorem OAI.LipschitzHilbert.SourceLatticePacket.frozen_reference_spectral_inputs line 67

Source documentation

Active frozen selector values give the required normalized spectra from just the original physical packet spectrum.

theorem frozen_reference_spectral_inputs {N : ℕ} {κ : Type} {ι : Fin N → Type}
    [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι)
    (c : ∀ j, ι j → κ → ℂ) (hc : ∀ j u k, ‖c j u k‖ ≤ 1)
    (t w cStar cEta CEta cb Cb : ℝ)
    (hw : 0 < w) (hcEta : 0 < cEta) (hcb : 0 ≤ cb) (hCb : 0 ≤ Cb)
    (hspectrum : ∀ j u k xi eta, planarAngularFourier (P.physicalPacket t j u k) (xi,eta) ≠ 0 →
      |xi+(t+P.rowSlope j)*eta| ≤ cStar/P.length j ∧ cEta ≤ w*eta ∧ w*eta ≤ CEta)
    (hselector : ∀ j u k, c j u k ≠ 0 →
      cb*w/P.length j ≤ |P.rowSlope j| ∧ |P.rowSlope j| ≤ Cb*w/P.length j) :
    (∀ j u k y xi,
      |xi| < (((cEta*cb-cStar)/(2*Real.pi))/(P.frozenProfile c hc).topLength)*(2:ℝ)^j.val →
      𝓕 ((P.frozenProfile c hc).raw 0 j u k y) xi = 0) ∧
…

Mentions: OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarAngularFourier, OAI.LipschitzHilbert.SourceLatticePacket.raw