SourceAngularScales.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Carrier spread and Fourier separation at the actual source block windows.

def OAI.LipschitzHilbert.AngularGrid.sourceGap line 16
Source documentation
The neighbor radius at the final transition, in child-width units.
```
def sourceGap (g : AngularGrid) (L : ℝ) (child : ℕ) : ℝ :=
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid
theorem OAI.LipschitzHilbert.AngularGrid.sourceGap_pos line 19

theorem OAI.LipschitzHilbert.AngularGrid.source_block_count_scales line 25

Source documentation

Both hypotheses of the separated-top count hold at the actual block neighbor radius, including the initial shorter block.

theorem source_block_count_scales (g : AngularGrid) (L : ℝ) {B : ℝ}
    (hB : 0 < B) (base child : ℕ) (hblock : g.width base ≤ B*g.width child) :
    (g.rootWidth/B^2)/(g.branching:ℝ)^child ≤ g.sourceGap L child/B^2 ∧
      g.width base ≤ B*g.sourceGap L child := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid

theorem OAI.LipschitzHilbert.AngularGrid.centers_close_in_ancestor line 41

theorem OAI.LipschitzHilbert.AngularGrid.source_block_carrier_mesh line 63

Source documentation

The full block length causes no loss in the carrier oscillation.

theorem source_block_carrier_mesh (g : AngularGrid) (L origin sR : ℝ)
    {w Cfreq eta : ℝ} (hw : 0 < w)
    (heta : |eta| ≤ Cfreq/w) (lower start : ℕ) (hle : lower ≤ start)
    (hbranch : (g.branching:ℝ) = SourceParameters.step L)
    (s t : ℝ) (hparent : g.index lower s = g.index lower t) :
    |(sR-g.center start (g.index start s))*eta-
      (sR-g.center start (g.index start t))*eta| *
      (sourceLineGrid L origin (sourceLineScale g L w start) (start-lower)
        (sourceLineScale_pos g L hw start)).meshWidth (start-lower) ≤
      (2*Cfreq)*SourceParameters.step L^(-(1/2:ℝ)) := by
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.sourceLineGrid, OAI.LipschitzHilbert.sourceLineScale, OAI.LipschitzHilbert.sourceLineScale_pos

theorem OAI.LipschitzHilbert.eventually_source_line_fourier_threshold line 88
Source documentation
Any fixed positive lower bound on transverse packet frequency suffices for the source Fourier gap at all sufficiently large parameters.
```
theorem eventually_source_line_fourier_threshold {c0 : ℝ} (hc0 : 0 < c0) :
    ∀ᶠ L : ℝ in atTop, ∀ (g : AngularGrid) (w : ℝ), 0 < w → ∀ level : ℕ,
      1/(sourceLineScale g L w level*SourceParameters.step L^(-(1/8:ℝ))) ≤
        (SourceParameters.step L^(3/4:ℝ)*g.width level)*(c0/w) := by
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.sourceLineScale, OAI.LipschitzHilbert.SourceParameters.step