LayerDiscrepancy.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sampling_measureReal_le_one line 10

theorem OAI.FiniteFactor.sampling_levelMass_measurable line 18

Source documentation

Joint superlevel probabilities are measurable in both thresholds.

theorem sampling_levelMass_measurable {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsFiniteMeasure μ] (f g : Ω → ℝ)
    (hf : Measurable f) (hg : Measurable g) :
    Measurable (fun p : ℝ × ℝ => (μ {x | p.1 ≤ f x ∧ p.2 ≤ g x}).toReal) := by
…

theorem OAI.FiniteFactor.sampling_layer_discrepancy line 41

Source documentation

Uniform superlevel discrepancy controls weighted pair integrals. The threshold square has area C^2; no density for the joint law is needed.

theorem sampling_layer_discrepancy {Ω Ψ : Type*} [MeasurableSpace Ω] [MeasurableSpace Ψ]
    (μ : Measure Ω) (ν : Measure Ψ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (f g : Ω → ℝ) (f₀ g₀ : Ψ → ℝ)
    (hf : Measurable f) (hg : Measurable g) (hf₀ : Measurable f₀) (hg₀ : Measurable g₀)
    (C δ : ℝ) (hC : 0 ≤ C)
    (hfb : ∀ x, 0 ≤ f x ∧ f x ≤ C) (hgb : ∀ x, 0 ≤ g x ∧ g x ≤ C)
    (hf₀b : ∀ x, 0 ≤ f₀ x ∧ f₀ x ≤ C) (hg₀b : ∀ x, 0 ≤ g₀ x ∧ g₀ x ≤ C)
    (hlevel : ∀ r t : ℝ, 0 < r → r ≤ C → 0 < t → t ≤ C →
      |(μ {x | r ≤ f x ∧ t ≤ g x}).toReal -
        (ν {x | r ≤ f₀ x ∧ t ≤ g₀ x}).toReal| ≤ δ) :
    |(∫ x, f x*g x ∂μ)-(∫ x, f₀ x*g₀ x ∂ν)| ≤ δ*C^2 := by
…