SourceLabeledMultiscaleEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The original finitely labeled family inherits multiscale synthesis through its exact slot partition. The only additional factor is the explicit fixed label bound, with no scale or vector-dimension loss.

def OAI.LipschitzHilbert.SourceLabeledLattice.physicalLabeledSynthesis line 17
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalLabeledSynthesis_memLp line 22
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalLabeledSynthesis_eq_slots line 27

theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_physical_labeled_multiscale_energy line 44

Source documentation

The annular constant is chosen before every packet family and label bound. Only nonzero coefficient coordinates need be separated.

theorem exists_physical_labeled_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) (Label : Fin N → Type)
      (Item : ∀ j, Label j → Type) [Fintype κ] [∀ j l, Fintype (Item j l)]
      (P : SourceLabeledLattice N κ Label Item) (B : ℕ),
      (∀ j, (P.labels j).card ≤ B) → ∀ (t w : ℝ), 0 < w →
    ∀ c : ∀ j (l : P.labels j), Item j l → EuclideanSpace ℂ κ,
      (∀ j l u k ξ η, planarAngularFourier (P.physicalPacket t j l u k) (ξ,η) ≠ 0 →
        |ξ+(t+P.rowSlope j l)*η| ≤ cStar/P.length j ∧
          cEta ≤ w*η ∧ w*η ≤ CEta) →
      (∀ j l u k, c j l u k ≠ 0 → cb*w/P.length j ≤ |P.rowSlope j l| ∧
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarAngularFourier