SourceBadEventUnion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finitely many deterministic residual events may be combined before selecting a spatial point or a mass cutoff.

theorem OAI.LipschitzHilbert.eventually_source_polynomial_exp line 17
Source documentation
Fixed polynomial losses are absorbed by one extra unit in the exponential decay rate.
```
theorem eventually_source_polynomial_exp (C a J : ℝ) (hC : 0 < C) :
    ∀ᶠ L : ℝ in atTop, C*L^a*Real.exp (-(J+1)*L) ≤ Real.exp (-J*L) := by
…
```

theorem OAI.LipschitzHilbert.source_bad_event_union line 36

Source documentation

Union measure on an actual interval, with the exact number of square/error/shift events retained until exponential absorption.

theorem source_bad_event_union {ι X : Type*} [MeasurableSpace X]
    (μ : Measure X) (events : Finset ι) (bad : ι → Set X) (δ : ℝ)
    (htail : ∀ i ∈ events, μ (bad i) ≤ ENNReal.ofReal δ*μ univ) :
    μ (⋃ i ∈ events, bad i) ≤ ENNReal.ofReal ((events.card:ℝ)*δ)*μ univ := by
…

theorem OAI.LipschitzHilbert.eventually_source_bad_event_tail line 52

Source documentation

The polynomial number of shift events loses one unit of exponential rate, uniformly in all measurable spaces and finite event lists.

theorem eventually_source_bad_event_tail (a J : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∀ (ι X : Type*) [MeasurableSpace X]
      (μ : Measure X) (events : Finset ι) (bad : ι → Set X),
      (events.card:ℝ) ≤ L^a →
      (∀ i ∈ events, μ (bad i) ≤ ENNReal.ofReal (Real.exp (-(J+1)*L))*μ univ) →
      μ (⋃ i ∈ events, bad i) ≤ ENNReal.ofReal (Real.exp (-J*L))*μ univ := by
…