OAI/Analysis/FourierLLogL/Fourier/Interval.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.FourierLLogL.Period.seg_eq_interval line 14
2. lemma OAI.FourierLLogL.Period.seg_translate_scale line 20
3. lemma OAI.FourierLLogL.Period.seg_translate_scale_rev line 25
4. lemma OAI.FourierLLogL.Period.mean_translate_scale line 33
5. lemma OAI.FourierLLogL.Period.seg_period_unit line 38
6. lemma OAI.FourierLLogL.Period.seg_period_int line 44
7. lemma OAI.FourierLLogL.Period.seg_integrable line 54
8. lemma OAI.FourierLLogL.Period.interval_integrable line 61
9. lemma OAI.FourierLLogL.Period.density_short line 68
10. theorem OAI.FourierLLogL.Period.density_good_set line 80

    Source documentation

    One good set works for all offsets and dilations of the grids.

    theorem density_good_set (ρ : ℝ → ℝ) (hρ : Measurable ρ) (hp : Periodic ρ 1)
        (h0 : ∀ x, 0 ≤ ρ x) (B : ℝ) (hb : ∀ x, ρ x ≤ B)
        (hm : (∫ x, ρ x ∂μ₁) ≤ 1) (D : ℝ) (hD : 0 < D) :
        ∃ G : Set ℝ, MeasurableSet G ∧ G ⊆ unitInt ∧
          μ₁ Gᶜ ≤ ENNReal.ofReal (64 / D) ∧
          ∀ x ∈ G, ∀ (a s : ℝ), 0 < s → s ≤ 1 → x ∈ Ico a (a+s) →
            (∫ y in Ico a (a+s), ρ y) ≤ D*s := by
    …

    Mentions: OAI.FourierLLogL.Period.μ₁, OAI.FourierLLogL.Period.unitInt