OAI/Analysis/LipschitzHilbert/Fourier/DyadicLineBad.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LipschitzHilbert.DyadicLineGrid.Bad line 17
2. theorem OAI.LipschitzHilbert.DyadicLineGrid.scale_le_iff line 20
3. theorem OAI.LipschitzHilbert.DyadicLineGrid.integrableOn_of_unit_bound line 23
4. theorem OAI.LipschitzHilbert.DyadicLineGrid.popular_interval_has_bad line 32

   Source documentation

   A popular interval fits in a bad dyadic interval, with only the factor-six loss in the average and with the prescribed upper scale.

   theorem popular_interval_has_bad {f : ℝ → ℝ} (hf : Measurable f)
       (hbound : ∀ x, 0 ≤ f x ∧ f x ≤ 1) {a b θ H : ℝ} {top : ℤ}
       (hab : a < b) (hθ : 0 ≤ θ) (hlen : b - a ≤ H) (htop : 6 * H ≤ scale top)
       (hpopular : θ * (b - a) ≤ ∫ x in Icc a b, f x) :
       ∃ q ∈ ({0, 1} : Finset ℤ), ∃ k j,
         k ≤ top ∧ Icc a b ⊆ cell q k j ∧ Bad q f (θ / 6) k j := by
   …

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

5. theorem OAI.LipschitzHilbert.DyadicLineGrid.popular_interval_has_maximalBad line 52

   Source documentation

   Hence every popular interval through a point is accounted for by a maximal bad interval in one of the two fixed grids.

   theorem popular_interval_has_maximalBad {f : ℝ → ℝ} (hf : Measurable f)
       (hbound : ∀ x, 0 ≤ f x ∧ f x ≤ 1) {a b θ H x : ℝ} {top : ℤ}
       (hab : a < b) (hθ : 0 ≤ θ) (hlen : b - a ≤ H) (htop : 6 * H ≤ scale top)
       (hx : x ∈ Icc a b) (hpopular : θ * (b - a) ≤ ∫ y in Icc a b, f y) :
       ∃ q ∈ ({0, 1} : Finset ℤ), ∃ k j,
         MaximalBad q top (Bad q f (θ / 6)) k j ∧ x ∈ cell q k j := by
   …

   Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale, OAI.LipschitzHilbert.DyadicLineGrid.MaximalBad, OAI.LipschitzHilbert.DyadicLineGrid.Bad, OAI.LipschitzHilbert.DyadicLineGrid.cell