SincMaskMotion.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Global motion of the actual sinc-product mask. The integral formula handles the origin without a quotient singularity.

theorem OAI.LipschitzHilbert.sinc_eq_integral_cos line 14
theorem OAI.LipschitzHilbert.abs_sinc_sub_sinc_le line 22
Source documentation
A global bound, including either endpoint equal to zero.
```
theorem abs_sinc_sub_sinc_le (x y : ℝ) :
    |Real.sinc x-Real.sinc y| ≤ |x-y| := by
…
```
theorem OAI.LipschitzHilbert.abs_sinc_product_sub_le line 44
theorem OAI.LipschitzHilbert.sincProductMask_motion line 61
theorem OAI.LipschitzHilbert.topSincMask_motion line 83
theorem OAI.LipschitzHilbert.topSincMask_motion_power line 93

theorem OAI.LipschitzHilbert.SlopeBox.mask_motion line 110

Source documentation

Motion in the two actual normalized coordinates of the top.

theorem mask_motion (T : SlopeBox) (L A : ℝ) (hL : 0 < L) (z₁ z₀ : ℝ × ℝ) :
    |T.mask L A z₁-T.mask L A z₀| ≤ (2*(⌈L⌉₊:ℝ)/L^A)*
      (|(z₁.1-z₀.1)/T.length|+
        |((z₁.2-z₀.2)-T.slope*(z₁.1-z₀.1))/T.width|) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox

theorem OAI.LipschitzHilbert.SlopeBox.mask_line_motion line 124