OAI/Analysis/LipschitzHilbert/Estimates/CountableCarleson.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Countable exhaustion of the Carleson tail

The count is an actual ENNReal sum over occurrences. Every finite subset has the same exponential tail bound, so continuity from below gives that bound for the full count without requiring a choice of enumeration.

  1. def OAI.LipschitzHilbert.occurrenceCount line 26
  2. def OAI.LipschitzHilbert.finiteOccurrenceCount line 29
  3. theorem OAI.LipschitzHilbert.measurable_occurrenceCount line 32
  4. theorem OAI.LipschitzHilbert.measurable_finiteOccurrenceCount line 37
  5. theorem OAI.LipschitzHilbert.finiteOccurrenceCount_nonneg line 42
  6. theorem OAI.LipschitzHilbert.finiteOccurrenceCount_mono line 49
  7. theorem OAI.LipschitzHilbert.ofReal_finiteOccurrenceCount line 56
  8. theorem OAI.LipschitzHilbert.occurrenceCount_superlevel_eq_iUnion line 67
  9. theorem OAI.LipschitzHilbert.occurrenceCount_tail_of_finite line 80

    Source documentation

    Uniform bounds on every finite subcount pass to the actual countable sum. This is the monotone-convergence step in count:line-lemma.

    theorem occurrenceCount_tail_of_finite (Q : ι → Set X) (μ : Measure X) [IsFiniteMeasure μ]
    {lambda B : ℝ} (hlambda : 0 ≤ lambda) (hB : 0 ≤ B)
    (hfinite : ∀ s : Finset ι, μ.real {x | lambda < finiteOccurrenceCount Q s x} ≤ B) :
    μ.real {x | ENNReal.ofReal lambda < occurrenceCount Q x} ≤ B := by
…

    Mentions: OAI.LipschitzHilbert.finiteOccurrenceCount, OAI.LipschitzHilbert.occurrenceCount

  10. theorem OAI.LipschitzHilbert.occurrenceCount_root_tail_of_finite line 100

    Source documentation

    The same exhaustion bound on a finite-measure root, even when the ambient measure is infinite, as for Lebesgue measure on the line.

    theorem occurrenceCount_root_tail_of_finite (Q : ι → Set X) (μ : Measure X)
    (hQ : ∀ i, MeasurableSet (Q i)) {P : Set X} (hPfinite : μ P ≠ ⊤)
    {lambda B : ℝ} (hlambda : 0 ≤ lambda) (hB : 0 ≤ B)
    (hfinite : ∀ s : Finset ι,
      μ.real ({x | lambda < finiteOccurrenceCount Q s x} ∩ P) ≤ B) :
    μ.real ({x | ENNReal.ofReal lambda < occurrenceCount Q x} ∩ P) ≤ B := by
…

    Mentions: OAI.LipschitzHilbert.finiteOccurrenceCount, OAI.LipschitzHilbert.occurrenceCount