LeanMachineLearning exposition

1.19. ForMathlib.Probability.WithDensity🔗

Lemmas about kernels and measures with density

Module LeanMachineLearning.ForMathlib.Probability.WithDensity contains 9 exposed declarations.

map_withDensity_comp🔗

LemmaMeasureTheory.map_withDensity_comp
Details

No docstring.

🔗theorem
MeasureTheory.map_withDensity_comp.{u_1, u_3} {α : Type u_1}
  {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  {μ : Measure α} {g : α → γ} {f : γ → ENNReal} (hg : Measurable g)
  (hf : Measurable f) :
  Measure.map g (Measure.withDensity μ (f ∘ g)) =
    Measure.withDensity (Measure.map g μ) f
MeasureTheory.map_withDensity_comp.{u_1,
    u_3}
  {α : Type u_1} {γ : Type u_3}
  {mα : MeasurableSpace α}
  {mγ : MeasurableSpace γ} {μ : Measure α}
  {g : α → γ} {f : γ → ENNReal}
  (hg : Measurable g)
  (hf : Measurable f) :
  Measure.map g
      (Measure.withDensity μ (f ∘ g)) =
    Measure.withDensity (Measure.map g μ)
      f

Code

lemma map_withDensity_comp {g : α → γ} {f : γ → ℝ≥0∞} (hg : Measurable g) (hf : Measurable f) :
    (μ.withDensity (f ∘ g)).map g = (μ.map g).withDensity f
Used by (2)

Actions: Source · Open Issue

Proof
by
  ext s hs
  rw [Measure.map_apply hg hs, withDensity_apply _ (hg hs), withDensity_apply _ hs,
    setLIntegral_map hs hf hg]
  rfl

map_equiv_withDensity🔗

LemmaMeasureTheory.map_equiv_withDensity
Details

No docstring.

🔗theorem
MeasureTheory.map_equiv_withDensity.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {μ : Measure α} {e : α ≃ᵐ β} {f : α → ENNReal} (hf : Measurable f) :
  Measure.map (⇑e) (Measure.withDensity μ f) =
    Measure.withDensity (Measure.map (⇑e) μ)
      (f ∘ ⇑(MeasurableEquiv.symm e))
MeasureTheory.map_equiv_withDensity.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α}
  {e : α ≃ᵐ β} {f : α → ENNReal}
  (hf : Measurable f) :
  Measure.map (⇑e)
      (Measure.withDensity μ f) =
    Measure.withDensity
      (Measure.map (⇑e) μ)
      (f ∘ ⇑(MeasurableEquiv.symm e))

Code

lemma map_equiv_withDensity {e : α ≃ᵐ β} {f : α → ℝ≥0∞} (hf : Measurable f) :
    (μ.withDensity f).map e = (μ.map e).withDensity (f ∘ e.symm)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  simp_rw [← map_withDensity_comp e.measurable (hf.comp e.symm.measurable),
    Function.comp_assoc, MeasurableEquiv.symm_comp_self]
  rfl

map_swap_withDensity_comp_snd🔗

LemmaMeasureTheory.map_swap_withDensity_comp_snd
Details

No docstring.

🔗theorem
MeasureTheory.map_swap_withDensity_comp_snd.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {μ : Measure (α × β)} {f : β → ENNReal} (hf : Measurable f) :
  Measure.map Prod.swap
      (Measure.withDensity μ fun ab => f (Prod.snd ab)) =
    Measure.withDensity (Measure.map Prod.swap μ) fun ba =>
      f (Prod.fst ba)
MeasureTheory.map_swap_withDensity_comp_snd.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {μ : Measure (α × β)} {f : β → ENNReal}
  (hf : Measurable f) :
  Measure.map Prod.swap
      (Measure.withDensity μ fun ab =>
        f (Prod.snd ab)) =
    Measure.withDensity
      (Measure.map Prod.swap μ) fun ba =>
      f (Prod.fst ba)

Code

lemma map_swap_withDensity_comp_snd {μ : Measure (α × β)} {f : β → ℝ≥0∞} (hf : Measurable f) :
    (μ.withDensity (fun ab ↦ f ab.2)).map Prod.swap =
      (μ.map Prod.swap).withDensity (fun ba ↦ f ba.1)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [← map_withDensity_comp measurable_swap (by fun_prop)]
  rfl

compProd_withDensity_left🔗

LemmaMeasureTheory.Measure.compProd_withDensity_left
Details

No docstring.

🔗theorem
MeasureTheory.Measure.compProd_withDensity_left.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α} [SFinite μ]
  {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : α → ENNReal}
  (hf : Measurable f) :
  compProd (withDensity μ f) κ =
    withDensity (compProd μ κ) fun ab => f (Prod.fst ab)
MeasureTheory.Measure.compProd_withDensity_left.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α}
  [SFinite μ]
  {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ]
  {f : α → ENNReal} (hf : Measurable f) :
  compProd (withDensity μ f) κ =
    withDensity (compProd μ κ) fun ab =>
      f (Prod.fst ab)

Code

lemma compProd_withDensity_left [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ] {f : α → ℝ≥0∞}
    (hf : Measurable f) : (μ.withDensity f) ⊗ₘ κ = (μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)
Used by (4)

Actions: Source · Open Issue

Proof
by
  refine ext_of_lintegral _ fun g hg ↦ ?_
  calc ∫⁻ ab, g ab ∂((μ.withDensity f) ⊗ₘ κ)
      = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂(μ.withDensity f) :=
        lintegral_compProd hg
    _ = ∫⁻ a, f a * ∫⁻ b, g (a, b) ∂κ a ∂μ :=
        lintegral_withDensity_eq_lintegral_mul _ hf hg.lintegral_kernel_prod_right'
    _ = ∫⁻ a, ∫⁻ b, f a * g (a, b) ∂κ a ∂μ :=
        lintegral_congr fun a ↦ (lintegral_const_mul _ (by fun_prop)).symm
    _ = ∫⁻ ab, (fun ab ↦ f ab.1) ab * g ab ∂(μ ⊗ₘ κ) :=
        (lintegral_compProd ((hf.comp measurable_fst).mul hg)).symm
    _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ κ).withDensity (fun ab ↦ f ab.1)) :=
        (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_fst) hg).symm

compProd_withDensity_withDensity🔗

LemmaMeasureTheory.Measure.compProd_withDensity_withDensity
Details

No docstring.

🔗theorem
MeasureTheory.Measure.compProd_withDensity_withDensity.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α} [SFinite μ]
  {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : α → ENNReal}
  {g : α → β → ENNReal} (hf : Measurable f)
  (hg : Measurable (Function.uncurry g))
  [ProbabilityTheory.IsSFiniteKernel
      (ProbabilityTheory.Kernel.withDensity κ g)] :
  compProd (withDensity μ f)
      (ProbabilityTheory.Kernel.withDensity κ g) =
    withDensity (compProd μ κ) fun ac =>
      f (Prod.fst ac) * g (Prod.fst ac) (Prod.snd ac)
MeasureTheory.Measure.compProd_withDensity_withDensity.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α}
  [SFinite μ]
  {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ]
  {f : α → ENNReal} {g : α → β → ENNReal}
  (hf : Measurable f)
  (hg : Measurable (Function.uncurry g))
  [ProbabilityTheory.IsSFiniteKernel
      (ProbabilityTheory.Kernel.withDensity
        κ g)] :
  compProd (withDensity μ f)
      (ProbabilityTheory.Kernel.withDensity
        κ g) =
    withDensity (compProd μ κ) fun ac =>
      f (Prod.fst ac) *
        g (Prod.fst ac) (Prod.snd ac)

Code

lemma compProd_withDensity_withDensity [SFinite μ] {κ : Kernel α β} [IsSFiniteKernel κ]
    {f : α → ℝ≥0∞} {g : α → β → ℝ≥0∞} (hf : Measurable f) (hg : Measurable (Function.uncurry g))
    [IsSFiniteKernel (κ.withDensity g)] :
    (μ.withDensity f) ⊗ₘ (κ.withDensity g) =
      (μ ⊗ₘ κ).withDensity (fun ac ↦ f ac.1 * g ac.1 ac.2)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [compProd_withDensity hg, compProd_withDensity_left hf]
  exact (withDensity_mul _ (hf.comp measurable_fst) hg).symm

compProd_eq_compProd_withDensity_comp_snd🔗

LemmaMeasureTheory.Measure.compProd_eq_compProd_withDensity_comp_snd
Details

No docstring.

🔗theorem
MeasureTheory.Measure.compProd_eq_compProd_withDensity_comp_snd.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α} [SFinite μ]
  {κ η : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η] {f : β → ENNReal}
  (hf : Measurable f)
  (h :
    ⇑κ =ᵐ[μ] ⇑(ProbabilityTheory.Kernel.withDensity η fun x b => f b)) :
  compProd μ κ = withDensity (compProd μ η) fun ab => f (Prod.snd ab)
MeasureTheory.Measure.compProd_eq_compProd_withDensity_comp_snd.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α}
  [SFinite μ]
  {κ η : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ]
  [ProbabilityTheory.IsSFiniteKernel η]
  {f : β → ENNReal} (hf : Measurable f)
  (h :
    ⇑κ =ᵐ[μ]
      ⇑(ProbabilityTheory.Kernel.withDensity
          η fun x b => f b)) :
  compProd μ κ =
    withDensity (compProd μ η) fun ab =>
      f (Prod.snd ab)

Code

lemma compProd_eq_compProd_withDensity_comp_snd [SFinite μ] {κ η : Kernel α β} [IsSFiniteKernel κ]
    [IsSFiniteKernel η] {f : β → ℝ≥0∞} (hf : Measurable f)
    (h : κ =ᵐ[μ] η.withDensity (fun _ b ↦ f b)) :
    μ ⊗ₘ κ = (μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2)
Used by (1)

Actions: Source · Open Issue

Proof
by
  /- A proof based on `compProd_congr` requires `IsSFiniteKernel (η.withDensity fun _ b ↦ f b)`. -/
  refine ext_of_lintegral _ fun g hg ↦ ?_
  calc ∫⁻ ab, g ab ∂(μ ⊗ₘ κ)
      = ∫⁻ a, ∫⁻ b, g (a, b) ∂κ a ∂μ :=
        lintegral_compProd hg
    _ = ∫⁻ a, ∫⁻ b, g (a, b) ∂((η a).withDensity f) ∂μ := by
        apply lintegral_congr_ae
        filter_upwards [h] with a ha
        rw [ha, Kernel.withDensity_apply _ (by fun_prop)]
    _ = ∫⁻ a, ∫⁻ b, f b * g (a, b) ∂η a ∂μ := by
        congr with a
        exact lintegral_withDensity_eq_lintegral_mul _ hf (by fun_prop)
    _ = ∫⁻ ab, f ab.2 * g ab ∂(μ ⊗ₘ η) :=
        (lintegral_compProd ((hf.comp measurable_snd).mul hg)).symm
    _ = ∫⁻ ab, g ab ∂((μ ⊗ₘ η).withDensity (fun ab ↦ f ab.2)) :=
        (lintegral_withDensity_eq_lintegral_mul _ (hf.comp measurable_snd) hg).symm

comp_withDensity_eq_withDensity_comp🔗

LemmaProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ENNReal}
  (hf : Measurable f) :
  MeasureTheory.Measure.bind μ ⇑(withDensity κ fun x b => f b) =
    MeasureTheory.Measure.withDensity (MeasureTheory.Measure.bind μ ⇑κ)
      f
ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {μ : MeasureTheory.Measure α}
  {κ : Kernel α β} [IsSFiniteKernel κ]
  {f : β → ENNReal} (hf : Measurable f) :
  MeasureTheory.Measure.bind μ
      ⇑(withDensity κ fun x b => f b) =
    MeasureTheory.Measure.withDensity
      (MeasureTheory.Measure.bind μ ⇑κ) f

Code

lemma comp_withDensity_eq_withDensity_comp {κ : Kernel α β} [IsSFiniteKernel κ] {f : β → ℝ≥0∞}
    (hf : Measurable f) : (κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ = (κ ∘ₘ μ).withDensity f
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine Measure.ext_of_lintegral _ fun g hg ↦ ?_
  calc ∫⁻ b, g b ∂((κ.withDensity (fun _ b ↦ f b)) ∘ₘ μ)
      = ∫⁻ a, ∫⁻ b, g b ∂(κ.withDensity (fun _ b ↦ f b)) a ∂μ :=
        Measure.lintegral_bind (measurable _).aemeasurable hg.aemeasurable
    _ = ∫⁻ a, ∫⁻ b, f b * g b ∂κ a ∂μ := by
        congr with a
        exact lintegral_withDensity _ (by fun_prop) _ hg
    _ = ∫⁻ b, f b * g b ∂(κ ∘ₘ μ) :=
        (Measure.lintegral_bind (measurable _).aemeasurable (hf.mul hg).aemeasurable).symm
    _ = ∫⁻ b, g b ∂((κ ∘ₘ μ).withDensity f) :=
        (lintegral_withDensity_eq_lintegral_mul _ hf hg).symm

compProd_withDensity_left🔗

LemmaProbabilityTheory.Kernel.compProd_withDensity_left
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.compProd_withDensity_left.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {κ : Kernel α β}
  {η : Kernel (α × β) γ} {f : α → β → ENNReal} [IsSFiniteKernel κ]
  [IsSFiniteKernel η] [IsSFiniteKernel (withDensity κ f)]
  (hf : Measurable (Function.uncurry f)) :
  compProd (withDensity κ f) η =
    withDensity (compProd κ η) fun a bc => f a (Prod.fst bc)
ProbabilityTheory.Kernel.compProd_withDensity_left.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {κ : Kernel α β} {η : Kernel (α × β) γ}
  {f : α → β → ENNReal}
  [IsSFiniteKernel κ] [IsSFiniteKernel η]
  [IsSFiniteKernel (withDensity κ f)]
  (hf : Measurable (Function.uncurry f)) :
  compProd (withDensity κ f) η =
    withDensity (compProd κ η) fun a bc =>
      f a (Prod.fst bc)

Code

lemma compProd_withDensity_left {κ : Kernel α β} {η : Kernel (α × β) γ} {f : α → β → ℝ≥0∞}
    [IsSFiniteKernel κ] [IsSFiniteKernel η] [IsSFiniteKernel (κ.withDensity f)]
    (hf : Measurable (Function.uncurry f)) :
    (κ.withDensity f) ⊗ₖ η = (κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  ext a : 1
  calc ((κ.withDensity f) ⊗ₖ η) a
      = (κ a).withDensity (f a) ⊗ₘ η.sectR a := by
        rw [compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ hf]
    _ = ((κ a) ⊗ₘ (η.sectR a)).withDensity (fun bc ↦ f a bc.1) :=
        Measure.compProd_withDensity_left (by fun_prop)
    _ = ((κ ⊗ₖ η).withDensity (fun a bc ↦ f a bc.1)) a := by
        rw [← compProd_apply_eq_compProd_sectR, Kernel.withDensity_apply _ (by fun_prop)]

withDensity_rnDeriv_eq'🔗

LemmaProbabilityTheory.Kernel.withDensity_rnDeriv_eq'
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {κ η : Kernel α β}
  [MeasurableSpace.CountableOrCountablyGenerated α β] [IsFiniteKernel κ]
  [IsFiniteKernel η]
  (h :
    ∀ (a : α), MeasureTheory.Measure.AbsolutelyContinuous (κ a) (η a)) :
  withDensity η (rnDeriv κ η) = κ
ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {κ η : Kernel α β}
  [MeasurableSpace.CountableOrCountablyGenerated
      α β]
  [IsFiniteKernel κ] [IsFiniteKernel η]
  (h :
    ∀ (a : α),
      MeasureTheory.Measure.AbsolutelyContinuous
        (κ a) (η a)) :
  withDensity η (rnDeriv κ η) = κ

Code

lemma withDensity_rnDeriv_eq' {κ η : Kernel α β} [MeasurableSpace.CountableOrCountablyGenerated α β]
    [IsFiniteKernel κ] [IsFiniteKernel η] (h : ∀ a, κ a ≪ η a) :
    η.withDensity (κ.rnDeriv η) = κ
Used by (1)

Actions: Source · Open Issue

Proof
Kernel.ext fun a ↦ withDensity_rnDeriv_eq (h a)
  1. MeasureTheory.map_withDensity_comp
  2. MeasureTheory.map_equiv_withDensity
  3. MeasureTheory.map_swap_withDensity_comp_snd
  4. MeasureTheory.Measure.compProd_withDensity_left
  5. MeasureTheory.Measure.compProd_withDensity_withDensity
  6. MeasureTheory.Measure.compProd_eq_compProd_withDensity_comp_snd
  7. ProbabilityTheory.Kernel.comp_withDensity_eq_withDensity_comp
  8. ProbabilityTheory.Kernel.compProd_withDensity_left
  9. ProbabilityTheory.Kernel.withDensity_rnDeriv_eq'