SourceFrozenSpectrum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Only a nonzero frozen selector needs annular separation. Zero selectors give zero packets, so empty scales and unused labels impose no artificial spectral hypothesis.

theorem OAI.LipschitzHilbert.SourceLatticePacket.frozenProfile_mainCoefficient line 21

Source documentation

Freezing a selector multiplies the original integral coefficient by its complex conjugate. The assertion includes zero selectors.

theorem frozenProfile_mainCoefficient (d : Fin N → ℝ) (v : ℝ×ℝ → ℝ)
    (g : ℝ×ℝ → EuclideanSpace ℂ κ) (j : Fin N) (u : ι j) (k : κ) :
    (P.frozenProfile c hc).family.mainCoefficient d v g j u k =
      conj (c j u k)*P.family.mainCoefficient d v g j u k := by
…

theorem OAI.LipschitzHilbert.SourceLatticePacket.frozenProfile_fourier_cutoffs line 48

Source documentation

The same physical spectral wedge supplies the annuli of every frozen raw jet. Separation is required precisely where the selector is nonzero, rather than on all unused packet labels.

theorem frozenProfile_fourier_cutoffs (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)
    (i : Fin 3) (j : Fin N) (u : ι j) (k : κ) (y : ℝ) :
    (∀ xi, |xi| < (((cEta*cb-cStar)/(2*Real.pi))/P.topLength)*(2:ℝ)^j.val →
      𝓕 ((P.frozenProfile c hc).raw i j u k y) xi = 0) ∧
    (∀ xi, (((CEta*Cb+cStar)/(2*Real.pi))/P.topLength)*(2:ℝ)^j.val < |xi| →
      𝓕 ((P.frozenProfile c hc).raw i j u k y) xi = 0) := by
…

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