OAI/Analysis/LipschitzHilbert/Packets/SourceFrozenCoefficientEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.analyzingCoefficient_l2_energy_le line 19

   Source documentation

   Finite weighted Bessel duality, applied to the exact analyzing integrals rather than an assumed coefficient estimate.

   theorem analyzingCoefficient_l2_energy_le
       {X I K : Type*} [MeasurableSpace X] [Fintype I] [Fintype K]
       (μ : Measure X) (area : I → ℝ) (wave : I → K → X → ℂ)
       (g : X → EuclideanSpace ℂ K) (A : ℝ) (hA : 0 ≤ A) (ha : ∀ i, 0 < area i)
       (hg : MemLp g 2 μ)
       (hint : ∀ i k, Integrable (fun x => g x k * conj (wave i k x)) μ)
       (hsyn : ∀ c, MemLp (diagonalSynthesis wave c) 2 μ)
       (hbound : ∀ c, (∫ x, ‖diagonalSynthesis wave c x‖^2 ∂μ) ≤
         A * ∑ i, area i * ‖c i‖^2) :
       (∑ i, area i * ‖analyzingCoefficient μ area wave g i‖^2) ≤
         A * ∫ x, ‖g x‖^2 ∂μ := by
   …

   Mentions: OAI.LipschitzHilbert.diagonalSynthesis, OAI.LipschitzHilbert.analyzingCoefficient

2. def OAI.LipschitzHilbert.SourceLabeledLattice.physicalFrozenCoefficient line 69
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalFrozenCoefficient_apply_eq_zero line 75
4. theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalFrozenCoefficient_eq_multiplier line 81
5. theorem OAI.LipschitzHilbert.SourceLabeledLattice.exists_physical_frozen_coefficient_energy line 90

   Source documentation

   Frozen selector values have a dimension-free Bessel bound on every finite selected packet family. Empty and zero-coefficient fibers need no selector separation.

   theorem exists_physical_frozen_coefficient_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 →
       ∀ (beta : P.PacketIndex → κ → ℂ) (packets : Finset P.PacketIndex)
         (g : ℝ×ℝ → EuclideanSpace ℂ κ),
         (∀ q ∈ packets, ∀ k, ‖beta q k‖ ≤ 1) → MemLp g 2 (volume.prod volume) →
         (∀ j l u k ξ η, planarAngularFourier (P.physicalPacket t j l u k) (ξ,η) ≠ 0 →
           |ξ+(t+P.rowSlope j l)*η| ≤ cStar/P.length j ∧
   …

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