FrequencySmoothing.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Actual smoothing from quantitative frequency-cut defects

The boundary approximants are constructed by the published nest distance theorem and the proved invariant averaging. The smoothing operators are their actual Poisson integrals; their inverse and algebra estimates use the published Hardy evaluation, with no additional analytic identities.

structure OAI.KadisonKastler.FrequencySmoothing line 32
Source documentation
The precise output of frequency-nest approximation for a contraction field. The approximation is on the common original Hilbert space.
```
structure FrequencySmoothing (F : ℝ → H →L[ℂ] H) (δ : ℝ) where
…
```
theorem OAI.KadisonKastler.exists_frequencySmoothing line 40
def OAI.KadisonKastler.FrequencySmoothing.smooth line 62
Source documentation
Positive-height smoothing after removing the scalar modulation.
```
def smooth (A : FrequencySmoothing F δ) (t r : ℝ) (hr : 0 < r) : H →L[ℂ] H :=
…
```
Mentions: OAI.KadisonKastler.FrequencySmoothing
theorem OAI.KadisonKastler.FrequencySmoothing.continuous_smooth line 65
theorem OAI.KadisonKastler.FrequencySmoothing.norm_smooth_le line 69
theorem OAI.KadisonKastler.FrequencySmoothing.norm_smooth_le_one_add line 73
theorem OAI.KadisonKastler.FrequencySmoothing.norm_product_sub_one_le line 84
theorem OAI.KadisonKastler.FrequencySmoothing.norm_smooth_sub_boundary_le line 109
Source documentation
Comparison to the original continuous modular field, using the same boundary Poisson operator that already has strong-star convergence.
```
theorem norm_smooth_sub_boundary_le
    (W : ℝ → unitary (H →L[ℂ] H))
    (A : FrequencySmoothing (modulatedUnitaryField W) δ)
    (hW : ∀ x, Continuous (fun t => (W t : H →L[ℂ] H) x))
    (hδ : 0 ≤ δ) (t r : ℝ) (hr : 0 < r) :
    ‖A.smooth t r hr - poissonBoundaryApprox W hW t r‖ ≤ Real.exp r * (2 * δ) :=
…
```
Mentions: OAI.KadisonKastler.FrequencySmoothing, OAI.KadisonKastler.modulatedUnitaryField, OAI.KadisonKastler.poissonBoundaryApprox
theorem OAI.KadisonKastler.FrequencySmoothing.norm_smooth_sub_boundary_le_four line 118
theorem OAI.KadisonKastler.FrequencySmoothing.infDist_smooth_sandwich_le line 132