restriction and normalized measure

Stream: Is there code for X?

[Pietro Lavino]

i want to formalize a probability measure given another probability measure and a measurable set a, which consists of the restriction of the first measure to a divided by measure of a ( measure of a \neq 0). this is what i have so far, is there an existing solution or a more convenient way to do this).

import Mathlib.Topology.Instances.Real
import Mathlib.Analysis.NormedSpace.FiniteDimension
import Mathlib.Analysis.Convolution
import Mathlib.MeasureTheory.Function.Jacobian
import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.SpecialFunctions.Log.ENNReal
import Mathlib.Data.ENNReal.Real
import Init.Data.Fin.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.Convex.Basic
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Ring
import Mathlib.MeasureTheory.Measure.NullMeasurable
import Mathlib.SetTheory.Cardinal.Basic
import Mathlib.Data.Finite.Card
import Mathlib.Analysis.Subadditive
import Mathlib.Analysis.SpecialFunctions.Log.NegMulLog


open MeasureTheory ENNReal Set Function BigOperators Finset

noncomputable def normalized_restriction {α : Type*} {m : MeasurableSpace α} {μ : Measure α} (a : Set α) (ha : MeasurableSet a) (hμa : μ a ≠ 0)(b: Set α): ENNReal := μ ( b ∩ a) / μ a

lemma normalized_empty {α : Type*} {m : MeasurableSpace α} {μ : Measure α} (a : Set α) (ha : MeasurableSet a) (hμa : μ a ≠ 0): normalized_restriction a ha hμa ∅ = 0 := by
 unfold normalized_restriction; simp

lemma normalized_restriction_nonneg {α : Type*} {m : MeasurableSpace α} {μ : Measure α} (a : Set α) (ha : MeasurableSet a) (hμa : μ a ≠ 0) (b : Set α): 0 ≤ normalized_restriction a ha hμa b  := by
  unfold normalized_restriction;simp

noncomputable def normalized_restrict  {α : Type*} {m : MeasurableSpace α} {μ : Measure α}(a : Set α) (ha : MeasurableSet a) (hμa : μ a ≠ 0) : Measure α
  where
measureOf:= λ s ↦  normalized_restriction a ha hμa s
empty:= by
  simp[normalized_empty]
mono := by
  intro s t hset
  dsimp; unfold normalized_restriction
  have :  μ (s ∩ a) ≤  μ (t ∩ a) := by
    refine OuterMeasureClass.measure_mono μ ?_
    · exact Set.inter_subset_inter hset fun ⦃a_1⦄ a => a
  exact ENNReal.div_le_div_right this (μ a)
iUnion_nat := by
  sorry
m_iUnion := by
  sorry
trim_le:= by

[Yaël Dillies]

This is docs#ProbabilityTheory.cond