SourceMaskGeometry.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The smallness of the actual top-mask derivative and Fourier radius follows from packet shortness and the fixed narrow cone. All scale parameters cancel before choosing the large manuscript parameter.

theorem OAI.LipschitzHilbert.SlopeBox.maskLineRate_packet_le line 15

theorem OAI.LipschitzHilbert.SlopeBox.scaled_maskLine_bounds line 41

Source documentation

A single scalar choice gives both derivative control and the half-annulus margin, uniformly over top lengths and packet scales.

theorem scaled_maskLine_bounds (T : SlopeBox) (L A t ell cone r lo : ℝ)
    (hL : 0 < L) (hell : 0 < ell) (hr : 0 < r) (hshort : ell ≤ T.length)
    (hcone : |t-T.slope| ≤ cone*T.width/ell)
    (hsmall : (2*(⌈L⌉₊:ℝ)/L^A)*(1+cone) ≤ min 1 (Real.pi*lo)) :
    2*(⌈L⌉₊:ℝ)*(|r*T.maskLineA L A|+|r*T.maskLineC L A t|) ≤ 1/(ell/r) ∧
    (2*(⌈L⌉₊:ℝ))*((|r*T.maskLineA L A|+|r*T.maskLineC L A t|)/(2*Real.pi)) ≤
      (lo/2)/(ell/r) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox

theorem OAI.LipschitzHilbert.SlopeBox.eventually_mask_scalar_small line 77
Source documentation
The source exponent A is fixed before choosing L. In particular no factor involving the number or lengths of packets enters this choice.
```
theorem eventually_mask_scalar_small {A cone lo : ℝ} (hA : 1 < A)
    (hcone : 0 ≤ cone) (hlo : 0 < lo) :
    ∀ᶠ L : ℝ in atTop,
      (2*(⌈L⌉₊:ℝ)/L^A)*(1+cone) ≤ min 1 (Real.pi*lo) := by
…
```