LayerCake.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sampling_integrable_bounded line 12

Source documentation

A bounded measurable real function on a finite measure space is integrable.

theorem sampling_integrable_bounded {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsFiniteMeasure μ] (f : Ω → ℝ) (hf : Measurable f)
    (C : ℝ) (hb : ∀ x, |f x| ≤ C) : Integrable f μ := by
…

theorem OAI.FiniteFactor.sampling_product_layerCake line 19

Source documentation

Finite layer-cake formula for a product, valid even for a singular joint law.

theorem sampling_product_layerCake {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsFiniteMeasure μ] (f 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) :
    (∫ x, f x*g x ∂μ) =
      ∫ r in Set.Ioc 0 C, ∫ t in Set.Ioc 0 C,
        (μ {x | r ≤ f x ∧ t ≤ g x}).toReal := by
…