OAI/Analysis/FiniteFactor/Sampling/SmoothedPair.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingSmooth_index_expansion line 10

   Source documentation

   The finite kernel index form, with total coefficient absolute sum at most H.

   theorem samplingSmooth_index_expansion (H : ℕ) (E : Set ℝ) (t : ℝ) :
       (samplingSmooth H E t : ℂ) = (H : ℂ)⁻¹ *
         ∑ p ∈ (Finset.range H).product (Finset.range H),
           samplingIntervalCoefficient E ((p.1 : ℤ)-(p.2 : ℤ)) *
             samplingCharacter ((p.1 : ℤ)-(p.2 : ℤ)) t := by
   …

   Mentions: OAI.FiniteFactor.samplingSmooth, OAI.FiniteFactor.samplingIntervalCoefficient, OAI.FiniteFactor.samplingCharacter

2. theorem OAI.FiniteFactor.samplingSmooth_constant_sum line 23
3. theorem OAI.FiniteFactor.samplingSmooth_pair_error line 32

   Source documentation

   Quantitative smoothed rectangle estimate, with the actual joint Fourier bound as the only dependence assumption.

   theorem samplingSmooth_pair_error {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
       (hX : Measurable X) (hY : Measurable Y) (H : ℕ) (hH : 0 < H)
       (E E' : Set ℝ) (ε : ℝ) (hε : 0 ≤ ε)
       (hFourier : ∀ v w : ℤ, |v| < (H : ℤ) → |w| < (H : ℤ) →
         (v ≠ 0 ∨ w ≠ 0) →
         ‖∫ θ, samplingCharacter v (X θ)*samplingCharacter w (Y θ) ∂μ‖ ≤ ε) :
       ‖(∫ θ, (samplingSmooth H E (X θ) : ℂ)*(samplingSmooth H E' (Y θ) : ℂ) ∂μ) -
         ((unitIntervalMeasure E).toReal : ℂ)*((unitIntervalMeasure E').toReal : ℂ)‖ ≤
         (H : ℝ)^2*ε := by
   …

   Mentions: OAI.FiniteFactor.samplingCharacter, OAI.FiniteFactor.samplingSmooth, OAI.FiniteFactor.unitIntervalMeasure