AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio

- The canonical real-valued Radon--Nikodym density representative used by ASTIS. The underlying measure-theoretic object remains Mathlib's ENNReal-valued `rnDeriv`; `toReal` is only the real representative needed by calculus.

noncomputable def density (mu pi : Measure α) (x : α) : ℝ :=
  (mu.rnDeriv pi x).toReal

/-- The canonical log-density ratio.  This is definitionally Mathlib's
log-likelihood ratio, so KL and Fisher layers share one representative. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:36published source at 0e31a3cda412

- The canonical log-density ratio. This is definitionally Mathlib's log-likelihood ratio, so KL and Fisher layers share one representative.

noncomputable def logRatio (mu pi : Measure α) : α → ℝ :=
  MeasureTheory.llr mu pi

@[simp]

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:41published source at 0e31a3cda412

No declaration docstring.

theorem logRatio_apply (mu pi : Measure α) (x : α) :
    logRatio mu pi x = Real.log (density mu pi x) := by
  rfl

@[fun_prop]

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:45published source at 0e31a3cda412

No declaration docstring.

theorem measurable_density (mu pi : Measure α) :
    Measurable (density mu pi) := by
  exact (Measure.measurable_rnDeriv mu pi).ennreal_toReal

@[fun_prop]

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:50published source at 0e31a3cda412

No declaration docstring.

theorem measurable_logRatio (mu pi : Measure α) :
    Measurable (logRatio mu pi) := by
  simpa [logRatio] using MeasureTheory.measurable_llr mu pi

/-- The real RN density is pointwise nonnegative. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:55published source at 0e31a3cda412

- The real RN density is pointwise nonnegative.

theorem density_nonneg (mu pi : Measure α) (x : α) :
    0 ≤ density mu pi x := by
  exact ENNReal.toReal_nonneg

/-- Absolute continuity makes the canonical real RN density positive `mu`-a.e.
The `rnDeriv < ∞` obligation is explicit because `toReal ∞ = 0`. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:60published source at 0e31a3cda412

- Absolute continuity makes the canonical real RN density positive `mu`-a.e. The `rnDeriv < ∞` obligation is explicit because `toReal ∞ = 0`.

theorem density_ae_pos_of_absolutelyContinuous
    (mu pi : Measure α) [SigmaFinite mu]
    [Measure.HaveLebesgueDecomposition mu pi]
    (hmuPi : mu ≪ pi) :
    ∀ᵐ x ∂mu, 0 < density mu pi x := by
  filter_upwards [Measure.rnDeriv_pos hmuPi,
    hmuPi.ae_le (Measure.rnDeriv_lt_top mu pi)] with x hxPos hxTop
  exact ENNReal.toReal_pos hxPos.ne' hxTop.ne

/-- Exponentiating the canonical log-density ratio recovers the canonical RN
density `mu`-a.e. under absolute continuity. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:66published source at 0e31a3cda412

- Exponentiating the canonical log-density ratio recovers the canonical RN density `mu`-a.e. under absolute continuity.

theorem exp_logRatio_ae_eq_density_of_absolutelyContinuous
    (mu pi : Measure α) [SigmaFinite mu]
    [Measure.HaveLebesgueDecomposition mu pi]
    (hmuPi : mu ≪ pi) :
    (fun x => Real.exp (logRatio mu pi x)) =ᵐ[mu] density mu pi := by
  filter_upwards [MeasureTheory.exp_llr_of_ac mu pi hmuPi] with x hx
  simpa [logRatio, density] using hx

/-- The canonical density of a measure relative to itself is one a.e. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:77published source at 0e31a3cda412

- The canonical density of a measure relative to itself is one a.e.

theorem density_self_ae (mu : Measure α) [SigmaFinite mu] :
    density mu mu =ᵐ[mu] fun _ => 1 := by
  filter_upwards [mu.rnDeriv_self] with x hx
  simp [density, hx]

/-- The canonical log-density ratio of a measure relative to itself is zero
a.e. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:86published source at 0e31a3cda412

- The canonical log-density ratio of a measure relative to itself is zero a.e.

theorem logRatio_self_ae (mu : Measure α) [SigmaFinite mu] :
    logRatio mu mu =ᵐ[mu] fun _ => 0 := by
  filter_upwards [MeasureTheory.llr_self mu] with x hx
  simpa [logRatio] using hx

/-- For probability measures, finite KL has the source-facing integral form

`KL(mu || pi) = integral log(d mu / d pi) dmu`

at the real-valued level.  Mathlib's `klDiv` remains the canonical ENNReal
measure divergence; this theorem is the bridge used by calculus arguments. -/

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:93published source at 0e31a3cda412

- For probability measures, finite KL has the source-facing integral form `KL(mu || pi) = integral log(d mu / d pi) dmu` at the real-valued level. Mathlib's `klDiv` remains the canonical ENNReal measure divergence; this theorem is the bridge used by calculus arguments.

theorem toReal_klDiv_eq_integral_logRatio_of_probability
    (mu pi : Measure α) [IsProbabilityMeasure mu] [IsProbabilityMeasure pi]
    (hmuPi : mu ≪ pi) :
    (_root_.InformationTheory.klDiv mu pi).toReal =
      ∫ x, logRatio mu pi x ∂mu := by
  simpa [logRatio] using
    (_root_.InformationTheory.toReal_klDiv_of_measure_eq
      (μ := mu) (ν := pi) hmuPi (by simp))

end

end RNLogRatio
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean:104published source at 0e31a3cda412