RootTailGluing.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Gluing rootwise counting tails on a bounded interval

Finite root covers and their total lengths transfer a rootwise tail to any bounded interval. The two shifted grids used by the covering lemma then combine by an exact ENNReal pigeonhole inequality.

theorem OAI.LipschitzHilbert.measureReal_le_sum_of_finite_cover line 23
theorem OAI.LipschitzHilbert.finite_root_tail_gluing line 33

theorem OAI.LipschitzHilbert.dyadic_root_tail_gluing line 51

Source documentation

Rootwise estimates combine with the actual floor-index root band.

theorem dyadic_root_tail_gluing (q k : ℤ) {a b : ℝ} (hab : a ≤ b)
    {E : Set ℝ} {c : ℝ} (hc : 0 ≤ c)
    (hroot : ∀ j ∈ DyadicLineGrid.rootBand q k a b,
      volume.real (E ∩ DyadicLineGrid.cell q k j) ≤
        c * volume.real (DyadicLineGrid.cell q k j)) :
    volume.real (E ∩ Set.Icc a b) ≤ c * (b - a + 2 * DyadicLineGrid.scale k) := by
…

Mentions: OAI.LipschitzHilbert.DyadicLineGrid.rootBand, OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.scale

theorem OAI.LipschitzHilbert.ennreal_two_count_superlevel line 63

theorem OAI.LipschitzHilbert.two_count_tail_gluing line 81

Source documentation

Adding the counts from two grids costs a factor two in both the front constant and the threshold.

theorem two_count_tail_gluing (μ : Measure X) {U : Set X} (hUfinite : μ U ≠ ⊤)
    (f g : X → ℝ≥0∞) {lambda B : ℝ} (hlambda : 0 ≤ lambda)
    (hf : μ.real ({x | ENNReal.ofReal (lambda / 2) < f x} ∩ U) ≤ B)
    (hg : μ.real ({x | ENNReal.ofReal (lambda / 2) < g x} ∩ U) ≤ B) :
    μ.real ({x | ENNReal.ofReal lambda < f x + g x} ∩ U) ≤ 2 * B := by
…

theorem OAI.LipschitzHilbert.two_dyadic_root_exponential_tail line 101

Source documentation

The rootwise Carleson tail on the two actual translated grids gives the full bounded-interval tail, with the threshold loss made explicit.

theorem two_dyadic_root_exponential_tail (k : ℤ) {a b A lambda : ℝ}
    (hab : a ≤ b) (hA : 0 < A) (hlambda : 0 ≤ lambda)
    (count : ℤ → ℝ → ℝ≥0∞)
    (hroot : ∀ q ∈ ({0, 1} : Finset ℤ), ∀ j ∈ DyadicLineGrid.rootBand q k a b,
      ∀ t : ℝ, 0 ≤ t →
      volume.real ({x | ENNReal.ofReal t < count q x} ∩ DyadicLineGrid.cell q k j) ≤
        2 * volume.real (DyadicLineGrid.cell q k j) * Real.exp (-t / (2 * A))) :
    volume.real ({x | ENNReal.ofReal lambda < count 0 x + count 1 x} ∩ Set.Icc a b) ≤
      4 * (b - a + 2 * DyadicLineGrid.scale k) * Real.exp (-lambda / (4 * A)) := by
…

Mentions: OAI.LipschitzHilbert.DyadicLineGrid.rootBand, OAI.LipschitzHilbert.DyadicLineGrid.cell, OAI.LipschitzHilbert.DyadicLineGrid.scale

theorem OAI.LipschitzHilbert.two_dyadic_root_exponential_tail_scale line 130

Source documentation

A root scale bounded by twelve times the allowed interval length gives an absolute global constant. This applies to exists_root_scale.

theorem two_dyadic_root_exponential_tail_scale (k : ℤ) {a b A H lambda : ℝ}
    (hab : a ≤ b) (hA : 0 < A) (hlambda : 0 ≤ lambda)
    (hscale : DyadicLineGrid.scale k ≤ 12 * H)
    (count : ℤ → ℝ → ℝ≥0∞)
    (hroot : ∀ q ∈ ({0, 1} : Finset ℤ), ∀ j ∈ DyadicLineGrid.rootBand q k a b,
      ∀ t : ℝ, 0 ≤ t →
      volume.real ({x | ENNReal.ofReal t < count q x} ∩ DyadicLineGrid.cell q k j) ≤
        2 * volume.real (DyadicLineGrid.cell q k j) * Real.exp (-t / (2 * A))) :
    volume.real ({x | ENNReal.ofReal lambda < count 0 x + count 1 x} ∩ Set.Icc a b) ≤
      96 * (b - a + H) * Real.exp (-lambda / (4 * A)) := by
…

Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale, OAI.LipschitzHilbert.DyadicLineGrid.rootBand, OAI.LipschitzHilbert.DyadicLineGrid.cell