OAI/Analysis/LipschitzHilbert/Phase/AngularSourceAmplitude.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.AngularGrid.sourceTransition line 17
2. def OAI.LipschitzHilbert.AngularGrid.sourcePacketBase line 23
3. def OAI.LipschitzHilbert.AngularGrid.sourcePacketAmplitude line 29
4. theorem OAI.LipschitzHilbert.AngularGrid.sourceTransition_norm_le_one line 37
5. theorem OAI.LipschitzHilbert.AngularGrid.sourceBoundaryMass_parent_le line 50
6. theorem OAI.LipschitzHilbert.AngularGrid.source_normalized_endpoint line 63

   Source documentation

   At equal real coordinates the packet coefficient is precisely the product of the parent-to-boundary ratios from the manuscript.

   theorem source_normalized_endpoint (g : AngularGrid) (tops : Finset ι)
       (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
       (hp : ∀ i ∈ tops, 0 ≤ precision i) (hw : ∀ i x, 0 < weight i x)
       {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (N : ℕ) (top : ι)
       (htop : top ∈ tops) (he : g.eligible cutoff (precision top) N) (a : ℝ) (x : X) :
       let n := fun j => g.mass tops slope precision cutoff weight j (g.index j (slope top)) x
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid

7. theorem OAI.LipschitzHilbert.AngularGrid.source_boundary_product_bounds line 94

   Source documentation

   Boundary coefficients always lie in the unit interval.

   theorem source_boundary_product_bounds (g : AngularGrid) (tops : Finset ι)
       (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
       (hp : ∀ i ∈ tops, 0 ≤ precision i) (hw : ∀ i x, 0 < weight i x)
       {K : ℕ} (hK : 0 < K) (gap : ℕ → ℝ) (N : ℕ) (top : ι)
       (htop : top ∈ tops) (he : g.eligible cutoff (precision top) N)
       (a : ℝ) (ha : 0 ≤ a) (x : X) :
       let c := ∏ j ∈ Finset.range N,
   …

   Mentions: OAI.LipschitzHilbert.AngularGrid