SourceLatticeMultiscaleEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The ordinary multiscale energy estimate for the original physical lattice packets. Residue coloring has a fixed cost determined only by the annular constants, not the number of lengths or vector bins.

theorem OAI.LipschitzHilbert.planarSchwartzSlice_sum_smul line 14

theorem OAI.LipschitzHilbert.SourceLatticePacket.raw_fourier_cutoffs_at line 27

Source documentation

The cutoff at one retained coefficient needs only that packet's selector separation; all other coefficients may vanish.

theorem raw_fourier_cutoffs_at (P : SourceLatticePacket N κ ι)
    (t w cStar cEta CEta cb Cb : ℝ) (hw : 0 < w)
    (hcEta : 0 < cEta) (hcb : 0 ≤ cb) (hCb : 0 ≤ Cb)
    (j : Fin N) (u : ι j) (k : κ)
    (hspectrum : ∀ ξ η, planarAngularFourier (P.physicalPacket t j u k) (ξ,η) ≠ 0 →
      |ξ+(t+P.rowSlope j)*η| ≤ cStar/P.length j ∧ cEta ≤ w*η ∧ w*η ≤ CEta)
    (hselector : cb*w/P.length j ≤ |P.rowSlope j| ∧ |P.rowSlope j| ≤ Cb*w/P.length j)
    (i : Fin 3) (y : ℝ) :
    (∀ ξ, |ξ| < (((cEta*cb-cStar)/(2*Real.pi))/P.topLength)*(2:ℝ)^j.val →
      𝓕 (P.raw i j u k y) ξ = 0) ∧
    (∀ ξ, (((CEta*Cb+cStar)/(2*Real.pi))/P.topLength)*(2:ℝ)^j.val < |ξ| →
      𝓕 (P.raw i j u k y) ξ = 0) := by
…

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

theorem OAI.LipschitzHilbert.SourceLatticePacket.physicalMultiscaleSynthesis_memLp line 57
Source documentation
The qualitative L² assertion accompanies the numerical estimate.
```
theorem physicalMultiscaleSynthesis_memLp (P : SourceLatticePacket N κ ι)
    (t : ℝ) (c : ∀ j, ι j → EuclideanSpace ℂ κ) :
    MemLp (fun z => ∑ j, planarFixedSynthesis (c j) (P.physicalPacket t j) z)
      2 (volume.prod volume) :=
…
```
Mentions: OAI.LipschitzHilbert.SourceLatticePacket, OAI.LipschitzHilbert.planarFixedSynthesis

theorem OAI.LipschitzHilbert.exists_physical_lattice_multiscale_energy line 67

Source documentation

The constant is fixed before every finite index type and packet family. Empty scales require no selector assumption.

theorem exists_physical_lattice_multiscale_energy
    (cStar cEta CEta cb Cb : ℝ) (hcEta : 0 < cEta)
    (hcb : 0 ≤ cb) (hCb : 0 ≤ Cb) (hgap : cStar < cEta*cb) :
    ∃ C : ℝ, 0 < C ∧ ∀ (N : ℕ) (κ : Type) (ι : Fin N → Type)
      [Fintype κ] [∀ j, Fintype (ι j)] (P : SourceLatticePacket N κ ι)
      (t w : ℝ), 0 < w →
    ∀ c : ∀ j, ι j → EuclideanSpace ℂ κ,
      (∀ j u k ξ η, planarAngularFourier (P.physicalPacket t j u k) (ξ,η) ≠ 0 →
        |ξ+(t+P.rowSlope j)*η| ≤ cStar/P.length j ∧
          cEta ≤ w*η ∧ w*η ≤ CEta) →
      (∀ j (u : ι j) k, c j u k ≠ 0 → cb*w/P.length j ≤ |P.rowSlope j| ∧
        |P.rowSlope j| ≤ Cb*w/P.length j) →
…

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