CellAverageOscillation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Complex cell averages and oscillation bounds

def OAI.JointDickman.complexCellAverage line 10
theorem OAI.JointDickman.complexCellAverage_norm_le line 13
theorem OAI.JointDickman.complexCellAverage_error line 26
Source documentation
No regularity of the signed mass is needed to replace a test by its cell average; only oscillation of the test enters.
```
theorem complexCellAverage_error {a b A x : ℝ} {F : ℝ → ℂ}
    (hab : a < b) (hF : IntervalIntegrable F volume a b)
    (hosc : ∀ y ∈ Set.Icc a b, ‖F x-F y‖ ≤ A) :
    ‖F x-complexCellAverage a b F‖ ≤ A := by
…
```
Mentions: OAI.JointDickman.complexCellAverage

theorem OAI.JointDickman.complexCellAverage_lipschitz_error line 46

Source documentation

A local Lipschitz estimate incurs at most L times the cell width.

theorem complexCellAverage_lipschitz_error {a b L x : ℝ} {F : ℝ → ℂ}
    (hab : a < b) (hL : 0 ≤ L) (hF : IntervalIntegrable F volume a b)
    (hx : x ∈ Set.Icc a b)
    (hLip : ∀ u ∈ Set.Icc a b, ∀ v ∈ Set.Icc a b,
      ‖F u-F v‖ ≤ L*|u-v|) :
    ‖F x-complexCellAverage a b F‖ ≤ L*(b-a) := by
…

Mentions: OAI.JointDickman.complexCellAverage