SourceBlockLineGrid.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The source line scales for a whole angular block. Refinement from the child scale to the parent scale cancels the angular branching exactly.

def OAI.LipschitzHilbert.sourceLineScale line 13
Source documentation
The manuscript line-window length at one angular generation.
```
def sourceLineScale (g : AngularGrid) (L w : ℝ) (level : ℕ) : ℝ :=
…
```
Mentions: OAI.LipschitzHilbert.AngularGrid
theorem OAI.LipschitzHilbert.sourceLineScale_pos line 16
theorem OAI.LipschitzHilbert.source_block_line_mesh line 22
theorem OAI.LipschitzHilbert.source_block_line_carrier line 37
theorem OAI.LipschitzHilbert.source_line_fourier_threshold line 55
Source documentation
At the source window size, the angular gap times the transverse frequency clears the exact Fourier threshold used by near-uniform averaging.
```
theorem source_line_fourier_threshold (g : AngularGrid) (L : ℝ)
    {w c0 : ℝ} (hw : 0 < w) (level : ℕ)
    (hc0 : SourceParameters.step L^(-(1/8:ℝ)) ≤ c0) :
    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.SourceParameters.step, OAI.LipschitzHilbert.sourceLineScale