IntervalSmoothing.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The endpoint error of a smoothed interval

A normalized integrable kernel approximates an interval indicator with error controlled by its two tails. The proof retains exact endpoints. This is the physical-space step of the Fourier truncation argument.

def OAI.CubicFirstMoment.intervalStep line 18
def OAI.CubicFirstMoment.intervalSmoothing line 20
theorem OAI.CubicFirstMoment.intervalStep_eq_of_away line 24
Source documentation
A shift smaller than the distance to both endpoints preserves membership.
```
theorem intervalStep_eq_of_away {a b s y : ℝ}
    (ha : |y| < |s - a|) (hb : |y| < |s - b|) :
    intervalStep a b (s - y) = intervalStep a b s := by
…
```
Mentions: OAI.CubicFirstMoment.intervalStep

theorem OAI.CubicFirstMoment.intervalStep_jump_le line 46

Source documentation

Any change in the indicator crosses at least one endpoint.

theorem intervalStep_jump_le (a b s y : ℝ) :
    |intervalStep a b s - intervalStep a b (s - y)| ≤
      (if |s - a| ≤ |y| then (1 : ℝ) else 0) +
      (if |s - b| ≤ |y| then (1 : ℝ) else 0) := by
…

Mentions: OAI.CubicFirstMoment.intervalStep

theorem OAI.CubicFirstMoment.integrable_intervalSmoothing_integrand line 60

theorem OAI.CubicFirstMoment.intervalSmoothing_error_le_tails line 75

Source documentation

The smoothed indicator has an error bounded by the kernel mass beyond the distances to the two endpoints. No positivity of the kernel is needed.

theorem intervalSmoothing_error_le_tails {k : ℝ → ℂ} (hk : Integrable k)
    (hmass : ∫ y, k y = 1) (a b s : ℝ) :
    ‖(intervalStep a b s : ℂ) - intervalSmoothing k a b s‖ ≤
      (∫ y, if |s-a| ≤ |y| then ‖k y‖ else 0) +
      (∫ y, if |s-b| ≤ |y| then ‖k y‖ else 0) := by
…

Mentions: OAI.CubicFirstMoment.intervalStep, OAI.CubicFirstMoment.intervalSmoothing