OAI/Analysis/LipschitzHilbert/Fourier/DyadicLineCount.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.DyadicLineGrid.measurableSet_bad line 18
2. theorem OAI.LipschitzHilbert.DyadicLineGrid.measurableSet_maximalBad line 24
3. abbrev OAI.LipschitzHilbert.DyadicLineGrid.Occurrence line 46
4. def OAI.LipschitzHilbert.DyadicLineGrid.selectedSet line 48
5. def OAI.LipschitzHilbert.DyadicLineGrid.selectedCount line 54
6. theorem OAI.LipschitzHilbert.DyadicLineGrid.measurableSet_selectedSet line 57
7. theorem OAI.LipschitzHilbert.DyadicLineGrid.measurable_selectedCount line 71
8. theorem OAI.LipschitzHilbert.DyadicLineGrid.card_le_selectedCount line 81
9. theorem OAI.LipschitzHilbert.DyadicLineGrid.popular_bins_card_le_selectedCount line 100

   Source documentation

   The one count dominates every finite family of distinct popular bins. The intervals may be chosen separately for each bin and point.

   theorem popular_bins_card_le_selectedCount (f : B → X × ℝ → ℝ)
       (hf : ∀ b, Measurable (f b))
       (hbound : ∀ b p, 0 ≤ f b p ∧ f b p ≤ 1)
       {θ H : ℝ} {top : ℤ} (hθ : 0 ≤ θ) (htop : 6 * H ≤ scale top)
       (p : X × ℝ) (bins : Finset B)
       (hpopular : ∀ b ∈ bins, ∃ a c : ℝ, a < c ∧ c - a ≤ H ∧ p.2 ∈ Icc a c ∧
         θ * (c - a) ≤ ∫ x in Icc a c, f b (p.1, x)) :
       (bins.card : ℝ≥0∞) ≤ selectedCount f top (θ / 6) p := by
   …

   Mentions: OAI.LipschitzHilbert.DyadicLineGrid.scale, OAI.LipschitzHilbert.DyadicLineGrid.selectedCount