Rectangle.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.integrable_unit_bounded line 11
theorem OAI.FiniteFactor.product_difference_unit_bound line 17

theorem OAI.FiniteFactor.integral_product_smoothing_error line 28

Source documentation

Uniform marginal smoothing errors control a product test under a possibly dependent joint law.

theorem integral_product_smoothing_error {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (f g a b : Ω → ℝ)
    (hf : Measurable f) (hg : Measurable g) (ha : Measurable a) (hb : Measurable b)
    (hfb : ∀ x, 0 ≤ f x ∧ f x ≤ 1) (hgb : ∀ x, 0 ≤ g x ∧ g x ≤ 1)
    (hab : ∀ x, 0 ≤ a x ∧ a x ≤ 1) (hbb : ∀ x, 0 ≤ b x ∧ b x ≤ 1) :
    |(∫ x, f x*g x ∂μ)-(∫ x, a x*b x ∂μ)| ≤
      (∫ x, |f x-a x| ∂μ)+(∫ x, |g x-b x| ∂μ) := by
…

theorem OAI.FiniteFactor.sampling_rectangle_discrepancy line 55

Source documentation

Explicit rectangle discrepancy derived from actual marginal domination and joint Fourier estimates. No two-dimensional density is required.

theorem sampling_rectangle_discrepancy {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] (X Y : Ω → ℝ)
    (hX : Measurable X) (hY : Measurable Y)
    (hdomX : μ.map X ≤ (2 : ℝ≥0∞) • unitIntervalMeasure)
    (hdomY : μ.map Y ≤ (2 : ℝ≥0∞) • unitIntervalMeasure)
    (H : ℕ) (hH : 0 < H) (a b a' b' δ ε : ℝ) (hδ : 0 < δ) (hε : 0 ≤ ε)
    (hFourier : ∀ v w : ℤ, |v| < (H : ℤ) → |w| < (H : ℤ) → (v ≠ 0 ∨ w ≠ 0) →
      ‖∫ θ, samplingCharacter v (X θ)*samplingCharacter w (Y θ) ∂μ‖ ≤ ε) :
    |(μ {θ | X θ ∈ Set.Icc a b ∧ Y θ ∈ Set.Icc a' b'}).toReal -
      (unitIntervalMeasure (Set.Icc a b)).toReal*(unitIntervalMeasure (Set.Icc a' b')).toReal| ≤
      24*δ+1/(2*(H : ℝ)*δ^2)+(H : ℝ)^2*ε := by
…

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