OneSidedCoboundary.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

One-sided integrable bounds for measurable coboundaries

The normalization transfer in the leaf-information identity need not be integrable. A one-sided integrable bound on its difference is sufficient.

lemma OAI.DukePrimeDegree.realClamp_monotone line 17
theorem OAI.DukePrimeDegree.integrable_coboundary_of_lower_bound line 21

theorem OAI.DukePrimeDegree.information_integrable_integral_of_coboundary line 84

Source documentation

A nonnegative information function differing from an integrable reference by a measurable coboundary has the same integral.

theorem information_integrable_integral_of_coboundary {Y : Type*} [MeasurableSpace Y]
    (μ : Measure Y) [IsFiniteMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) {f J I : Y → ℝ}
    (hf : StronglyMeasurable f) (hJ : Integrable J μ)
    (hI : ∀ᵐ y ∂μ, 0 ≤ I y)
    (heq : I =ᵐ[μ] fun y => J y + (f y-f (T y))) :
    Integrable I μ ∧ (∫ y, I y ∂μ) = ∫ y, J y ∂μ := by
…

theorem OAI.DukePrimeDegree.information_integrable_integral_of_ae_coboundary line 100

Source documentation

Null-set changes in the transfer do not affect the information identity.

theorem information_integrable_integral_of_ae_coboundary {Y : Type*} [MeasurableSpace Y]
    (μ : Measure Y) [IsFiniteMeasure μ] {T : Y → Y}
    (hT : MeasurePreserving T μ μ) {f J I : Y → ℝ}
    (hf : AEStronglyMeasurable f μ) (hJ : Integrable J μ)
    (hI : ∀ᵐ y ∂μ, 0 ≤ I y)
    (heq : I =ᵐ[μ] fun y => J y + (f y-f (T y))) :
    Integrable I μ ∧ (∫ y, I y ∂μ) = ∫ y, J y ∂μ := by
…