OAI/Analysis/LipschitzHilbert/Trees/SourceSnapshotSize.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SlopeBox.weight_le_two_pow line 15
2. theorem OAI.LipschitzHilbert.SourceLabeledLattice.restrictCoefficient_full line 28
3. theorem OAI.LipschitzHilbert.SourceLabeledLattice.rawBand_coeff_real_smul line 34
4. theorem OAI.LipschitzHilbert.AngularGrid.source_snapshot_masked_node_bound line 49

   Source documentation

   Full length range, with the actual endpoint masks placed in the original coefficients. No bound on the number of tops is used.

   theorem source_snapshot_masked_node_bound {ι X : Type*}
       (grid : AngularGrid) (tops : Finset ι) (slope precision : ι → ℝ) (cutoff : ℝ)
       (weight : ι → X → ℝ) (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t z, 0 < weight t z)
       {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (phase : ℕ → ℂ)
       (M : ι → ℕ) (hM : ∀ t ∈ tops, grid.eligible cutoff (precision t) (M t))
       (hMmax : ∀ t ∈ tops, ∀ k, grid.eligible cutoff (precision t) k → k ≤ M t)
       (a Z : ℝ) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) (hZ : 0 ≤ Z)
       (hz0 : ∀ t ∈ tops, ∀ j < M t, 0 ≤ (phase j).re)
       (hz : ∀ t ∈ tops, ∀ j < M t, ‖phase j‖ ≤ Z)
       {N : ℕ} {κ : Type} {Label : Fin N → Type} {Item : ∀ j, Label j → Type}
       [Fintype κ] [∀ j l, Fintype (Item j l)]
       (P : ι → SourceLabeledLattice N κ Label Item)
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceLabeledLattice

5. theorem OAI.LipschitzHilbert.source_snapshot_normalized_size line 94
6. theorem OAI.LipschitzHilbert.source_snapshot_coefficient_mass line 112

   Source documentation

   The off-path coefficient budget contains the sum of its actual child fractions, so it vanishes with the relative path drop.

   theorem source_snapshot_coefficient_mass {ι : Type*} [Fintype ι]
       (c : ι → ℝ) (A : ι → E) (lam : ι → ℂ) (n μ C u : ℝ)
       (hn : 0 < n) (hc : ∀ i, 0 < c i) (hC : 0 ≤ C)
       (hA : ∀ i, ‖A i‖ ≤ C*c i) (hlam : ∀ i, ‖lam i‖ ≤ 1)
       (hmass : ∑ i, c i/n ≤ u) :
       (∑ i, ‖((((c i/n)^(1-μ):ℝ):ℂ)*lam i) •
         (((c i^(μ-1):ℝ):ℂ) • A i)‖) ≤ (C*n^μ)*u := by
   …