Kernel with two values

def ProbabilityTheory.twoHypKernel {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) : ProbabilityTheory.Kernel Bool 𝒳

The kernel that sends false to μ and true to ν.

Equations

• ProbabilityTheory.twoHypKernel μ ν = { toFun := fun (b : Bool) => bif b then ν else μ, measurable' := ⋯ }

@[simp]

theorem ProbabilityTheory.twoHypKernel_true {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} : (ProbabilityTheory.twoHypKernel μ ν) true = ν

@[simp]

theorem ProbabilityTheory.twoHypKernel_false {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} : (ProbabilityTheory.twoHypKernel μ ν) false = μ

@[simp]

theorem ProbabilityTheory.twoHypKernel_apply {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} (b : Bool) : (ProbabilityTheory.twoHypKernel μ ν) b = bif b then ν else μ

instance ProbabilityTheory.instIsFiniteKernelBoolTwoHypKernelOfIsFiniteMeasure {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.twoHypKernel μ ν)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.instIsMarkovKernelBoolTwoHypKernelOfIsProbabilityMeasure {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.twoHypKernel μ ν)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.Kernel_bool_eq_twoHypKernel {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (κ : ProbabilityTheory.Kernel Bool 𝒳) : κ = ProbabilityTheory.twoHypKernel (κ false) (κ true)

@[simp]

theorem ProbabilityTheory.comp_twoHypKernel {𝒳 : Type u_2} {𝒴 : Type u_4} {m𝒳 : MeasurableSpace 𝒳} {m𝒴 : MeasurableSpace 𝒴} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} (κ : ProbabilityTheory.Kernel 𝒳 𝒴) : κ.comp (ProbabilityTheory.twoHypKernel μ ν) = ProbabilityTheory.twoHypKernel (μ.bind ⇑κ) (ν.bind ⇑κ)

theorem ProbabilityTheory.measure_comp_twoHypKernel {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν) = π {true} • ν + π {false} • μ

theorem ProbabilityTheory.absolutelyContinuous_measure_comp_twoHypKernel_left {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) {π : MeasureTheory.Measure Bool} (hπ : π {false} ≠ 0) : μ.AbsolutelyContinuous (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν))

theorem ProbabilityTheory.absolutelyContinuous_measure_comp_twoHypKernel_right {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) {π : MeasureTheory.Measure Bool} (hπ : π {true} ≠ 0) : ν.AbsolutelyContinuous (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν))

theorem ProbabilityTheory.sum_smul_rnDeriv_twoHypKernel {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : π {true} • ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) + π {false} • μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) =ᵐ[π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)] 1

theorem ProbabilityTheory.sum_smul_rnDeriv_twoHypKernel' {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : ∀ᵐ (x : 𝒳) ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν), π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x + π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x = 1

noncomputable def ProbabilityTheory.twoHypKernelInv {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) : ProbabilityTheory.Kernel 𝒳 Bool

The kernel from 𝒳 to Bool defined by x ↦ (π₀ * ∂μ/∂(twoHypKernel μ ν ∘ₘ π) x + π₁ * ∂ν/∂(twoHypKernel μ ν ∘ₘ π) x). It is the Bayesian inverse of twoHypKernel μ ν with respect to π (see bayesInv_twoHypKernel).

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.twoHypKernelInv_apply {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) (π : MeasureTheory.Measure Bool) (x : 𝒳) : (ProbabilityTheory.twoHypKernelInv μ ν π) x = if π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x + π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x = 1 then (π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x) • MeasureTheory.Measure.dirac true + (π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x) • MeasureTheory.Measure.dirac false else MeasureTheory.Measure.dirac true

theorem ProbabilityTheory.twoHypKernelInv_apply_ae {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : ∀ᵐ (x : 𝒳) ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν), (ProbabilityTheory.twoHypKernelInv μ ν π) x = (π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x) • MeasureTheory.Measure.dirac true + (π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x) • MeasureTheory.Measure.dirac false

theorem ProbabilityTheory.twoHypKernelInv_apply' {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] (s : Set Bool) : ∀ᵐ (x : 𝒳) ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν), ((ProbabilityTheory.twoHypKernelInv μ ν π) x) s = π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x * s.indicator 1 true + π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x * s.indicator 1 false

theorem ProbabilityTheory.twoHypKernelInv_apply_false {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : ∀ᵐ (x : 𝒳) ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν), ((ProbabilityTheory.twoHypKernelInv μ ν π) x) {false} = π {false} * μ.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x

theorem ProbabilityTheory.twoHypKernelInv_apply_true {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : ∀ᵐ (x : 𝒳) ∂π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν), ((ProbabilityTheory.twoHypKernelInv μ ν π) x) {true} = π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)) x

instance ProbabilityTheory.instIsMarkovKernelBoolTwoHypKernelInv {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {μ : MeasureTheory.Measure 𝒳} {ν : MeasureTheory.Measure 𝒳} (π : MeasureTheory.Measure Bool) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.twoHypKernelInv μ ν π)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.measure_prod_ext {𝒳 : Type u_2} {𝒴 : Type u_4} {m𝒳 : MeasurableSpace 𝒳} {m𝒴 : MeasurableSpace 𝒴} {μ : MeasureTheory.Measure (𝒳 × 𝒴)} {ν : MeasureTheory.Measure (𝒳 × 𝒴)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (A : Set 𝒳), MeasurableSet A → ∀ (B : Set 𝒴), MeasurableSet B → μ (A ×ˢ B) = ν (A ×ˢ B)) : μ = ν

theorem ProbabilityTheory.bayesInv_twoHypKernel {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} (μ : MeasureTheory.Measure 𝒳) (ν : MeasureTheory.Measure 𝒳) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] : ⇑(ProbabilityTheory.bayesInv (ProbabilityTheory.twoHypKernel μ ν) π) =ᵐ[π.bind ⇑(ProbabilityTheory.twoHypKernel μ ν)] ⇑(ProbabilityTheory.twoHypKernelInv μ ν π)

theorem ProbabilityTheory.bayesRiskPrior_eq_of_hasGenBayesEstimator_binary {𝒳 : Type u_2} {m𝒳 : MeasurableSpace 𝒳} {𝒴 : Type u_6} {𝒵 : Type u_7} [MeasurableSpace 𝒴] [MeasurableSpace 𝒵] (E : ProbabilityTheory.estimationProblem Bool 𝒴 𝒵) (P : ProbabilityTheory.Kernel Bool 𝒳) [ProbabilityTheory.IsFiniteKernel P] (π : MeasureTheory.Measure Bool) [MeasureTheory.IsFiniteMeasure π] [h : ProbabilityTheory.HasGenBayesEstimator E P π] : ProbabilityTheory.bayesRiskPrior E P π = ∫⁻ (x : 𝒳), ⨅ (z : 𝒵), π {true} * (P true).rnDeriv (π.bind ⇑P) x * E.ℓ (E.y true, z) + π {false} * (P false).rnDeriv (π.bind ⇑P) x * E.ℓ (E.y false, z) ∂π.bind ⇑P