ReferenceFamilyException.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The common counting exceptional set

One count is chosen for each reference top, independently of every separated list. Their finite union has the total-top-area budget of §6.

def OAI.LipschitzHilbert.referenceFamilyException line 20
theorem OAI.LipschitzHilbert.measurableSet_referenceFamilyException line 24
theorem OAI.LipschitzHilbert.referenceFamilyException_measure_ne_top line 32
Source documentation
The actual exceptional union has finite measure, since each of its reference charts is supported on a bounded rectangle.
```
theorem referenceFamilyException_measure_ne_top {ι : Type*} [Fintype ι]
    (T : ι → SlopeBox) (N : ι → ℝ × ℝ → ℝ≥0∞) (K lambda : ℝ) :
    (volume.prod volume) (referenceFamilyException T N K lambda) ≠ ∞ := by
…
```
Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.referenceFamilyException

theorem OAI.LipschitzHilbert.count_le_outside_referenceFamilyException line 48

Source documentation

Outside the single union, every significant reference has its count bounded by the same threshold.

theorem count_le_outside_referenceFamilyException {ι : Type*}
    (T : ι → SlopeBox) (N : ι → ℝ × ℝ → ℝ≥0∞) {K lambda : ℝ}
    {z : ℝ × ℝ} (hout : z ∉ referenceFamilyException T N K lambda)
    (i : ι) (hsignificant : (T i).radius z ≤ K) :
    N i (((T i).referenceChart.symm z).2, z.1) ≤ ENNReal.ofReal lambda := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.referenceFamilyException

theorem OAI.LipschitzHilbert.referenceFamilyException_measure_bound line 57

theorem OAI.LipschitzHilbert.reference_family_count_setup line 79

Source documentation

Actual reference counts exist simultaneously for the finite top family. The counts are fixed before the threshold and before the list.

theorem reference_family_count_setup {ι : Type*} [Fintype ι]
    (T : ι → SlopeBox) (u : ℝ × ℝ → ℝ) (hu : Measurable u)
    {M : ℕ} (hM : 0 < M) {c K P θ : ℝ} (hc : 0 ≤ c) (hcM : c ≤ M)
    (hK : 0 ≤ K) (hP : 0 < P) (hθ : 0 < θ) :
    ∃ N : ι → ℝ × ℝ → ℝ≥0∞, (∀ i, Measurable (N i)) ∧
      (∀ i, (T i).ReferencePopularCount u c P θ M (N i)) ∧
      ∀ lambda : ℝ, 0 ≤ lambda →
        MeasurableSet (referenceFamilyException T N K lambda) ∧
        (volume.prod volume).real (referenceFamilyException T N K lambda) ≤
          (∑ i, (T i).length * (T i).width) *
            (384 * K * (K + P) * Real.exp (-θ * lambda / (240 * (1 + c)))) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.referenceFamilyException

theorem OAI.LipschitzHilbert.referenceFamilyException_exponential_budget line 100

Source documentation

A polynomial prefactor in the family-area estimate is absorbed by the Gaussian tail, giving exactly the requested S exp(-J L) budget.

theorem referenceFamilyException_exponential_budget {ι : Type*} [Fintype ι]
    (T : ι → SlopeBox) (E : Set (ℝ × ℝ)) {C c J a L : ℝ}
    (hC : 0 < C) (hc : 0 < c) (hL : 1 ≤ L)
    (hlarge : (|Real.log C| + |a| + J) / c ≤ L)
    (hmeasure : (volume.prod volume).real E ≤
      (∑ i, (T i).length * (T i).width) * (C * L ^ a * Real.exp (-c * L ^ 2))) :
    (volume.prod volume).real E ≤
      (∑ i, (T i).length * (T i).width) * Real.exp (-J * L) := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox