OAI/Analysis/FiniteFactor/Sampling/FourierSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingCharacter_product_integrable line 11

   Source documentation

   Bounded characters are integrable under every probability law.

   theorem samplingCharacter_product_integrable {Ω : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
       (hX : Measurable X) (hY : Measurable Y) (v w : ℤ) :
       Integrable (fun θ => samplingCharacter v (X θ)*samplingCharacter w (Y θ)) μ := by
   …

   Mentions: OAI.FiniteFactor.samplingCharacter

2. theorem OAI.FiniteFactor.samplingFourier_sum_error line 22

   Source documentation

   Finite Fourier polynomials require only Fourier bounds on the actual joint law; the two input phases need not be independent.

   theorem samplingFourier_sum_error {Ω α β : Type*} [MeasurableSpace Ω]
       (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
       (hX : Measurable X) (hY : Measurable Y)
       (F : Finset α) (G : Finset β) (v : α → ℤ) (w : β → ℤ)
       (A : α → ℂ) (B : β → ℂ)
       (hA : ∀ a ∈ F, ‖A a‖ ≤ 1) (hB : ∀ b ∈ G, ‖B b‖ ≤ 1)
       (ε : ℝ) (hε : 0 ≤ ε)
       (hFourier : ∀ a ∈ F, ∀ b ∈ G, v a ≠ 0 ∨ w b ≠ 0 →
         ‖∫ θ, samplingCharacter (v a) (X θ)*samplingCharacter (w b) (Y θ) ∂μ‖ ≤ ε) :
       ‖(∫ θ, (∑ a ∈ F, A a*samplingCharacter (v a) (X θ)) *
             (∑ b ∈ G, B b*samplingCharacter (w b) (Y θ)) ∂μ) -
         (∑ a ∈ F, if v a = 0 then A a else 0) *
   …

   Mentions: OAI.FiniteFactor.samplingCharacter