mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
⊢ (∀ (q : ℚ), f (a, t) q ≤ 1) → ‖⨅ r, f (a, t) ↑r‖ ≤ 1

Tactic:
h_le_one

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ‖⨅ r, f (a, t) ↑r‖ ≤ 1
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
⊢ (⇑κ ∘ₘ μ).prod ν = ⇑(κ ∥ₖ Kernel.id) ∘ₘ μ.prod ν

Tactic:
by
  have h1 : (κ ∘ₘ μ).prod ν = (ν.prod (κ ∘ₘ μ)).map Prod.swap := by rw [Measure.prod_swap]
  have h2 : (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν) = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
    calc (κ ∥ₖ Kernel.id) ∘ₘ (μ.prod ν)
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((ν.prod μ).map Prod.swap) := by rw [Measure.prod_swap]
    _ = (κ ∥ₖ Kernel.id) ∘ₘ ((Kernel.swap _ _) ∘ₘ (ν.prod μ)) := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
    _ = (Kernel.swap _ _) ∘ₘ ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)) := by
      rw [Measure.comp_assoc, Measure.comp_assoc, Kernel.swap_parallelComp]
    _ = ((Kernel.id ∥ₖ κ) ∘ₘ (ν.prod μ)).map Prod.swap := by
      rw [Kernel.swap, Measure.deterministic_comp_eq_map]
  rw [← Measure.prod_comp_right, ← h1] at h2
  exact h2.symm

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case h.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ MemLp (⇑L ∘ (Y - X)) 2 P

pp: case h.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ (⇑L ∘ X) ⟂ᵢ[P] ⇑L ∘ (Y - X)

pp: case h.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (⇑L ∘ X) P

pp: case h.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (⇑L ∘ (Y - X)) P

Tactic:
· rw [map_comp_sub]
    exact (hY.map L).memLp_two.sub (hX.map L).memLp_two

Goal state after:
case h.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ (⇑L ∘ X) ⟂ᵢ[P] ⇑L ∘ (Y - X)

case h.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (⇑L ∘ X) P

case h.hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
X Y : Ω → E
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
h : X ⟂ᵢ[P] Y - X
this : IsProbabilityMeasure P
L : StrongDual ℝ E
⊢ Integrable (⇑L ∘ (Y - X)) P
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t

Tactic:
apply MeasurableSpace.ae_induction_on_inter Real.borel_eq_generateFrom_Iic_rat
    Real.isPiSystem_Iic_rat

Goal state after:
case h_empty
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, (κ x) ∅ = (ρ.condKernel x) ∅

case h_basic
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ t ∈ ⋃ a, {Iic ↑a}, (κ x) t = (ρ.condKernel x) t

case h_compl
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ (t : Set ℝ), MeasurableSet t → (κ x) t = (ρ.condKernel x) t → (κ x) tᶜ = (ρ.condKernel x) tᶜ

case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (f : ℕ → Set ℝ),
      Pairwise (Function.onFun Disjoint f) →
        (∀ (i : ℕ), MeasurableSet (f i)) →
          (∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)) → (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
X' : α → β
Y' : α → Ω
hY : Y =ᵐ[μ] Y'
hX : X =ᵐ[μ] X'
a : α
ha : X a = X' a
⊢ Y a = Y' a → (X a, Y a) = (X' a, Y' a)

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
X' : α → β
Y' : α → Ω
hY : Y =ᵐ[μ] Y'
hX : X =ᵐ[μ] X'
a : α
ha : X a = X' a
hb : Y a = Y' a
⊢ (X a, Y a) = (X' a, Y' a)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
X' : α → β
Y' : α → Ω
hY : Y =ᵐ[μ] Y'
hX : X =ᵐ[μ] X'
a : α
ha : X a = X' a
hb : Y a = Y' a
⊢ (X' a, Y a) = (X' a, Y' a)

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
X' : α → β
Y' : α → Ω
hY : Y =ᵐ[μ] Y'
hX : X =ᵐ[μ] X'
a : α
ha : X a = X' a
hb : Y a = Y' a
⊢ (X' a, Y' a) = (X' a, Y' a)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
⊢ ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑κ

Tactic:
by_cases hX : AEMeasurable X μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : AEMeasurable X μ
⊢ ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑κ

case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
X : α → β
hY : AEMeasurable Y μ
κ : Kernel β Ω
inst✝ : IsFiniteKernel κ
hκ : Measure.map (fun x ↦ (X x, Y x)) μ = Measure.map X μ ⊗ₘ κ
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑κ
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)

Tactic:
by_cases hX : AEMeasurable X μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)

case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
Ω' : Type u_5
mΩ' : MeasurableSpace Ω'
inst✝¹ : StandardBorelSpace Ω'
inst✝ : Nonempty Ω'
X : α → β
hY : AEMeasurable Y μ
f : Ω → Ω'
hf : Measurable f
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ Y) X μ) =ᵐ[Measure.map X μ] ⇑((condDistrib Y X μ).map f)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)

Tactic:
by_cases hX : AEMeasurable X μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)

case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
f : β → Ω
hf : Measurable f
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (f ∘ X) X μ) =ᵐ[Measure.map X μ] ⇑(Kernel.deterministic f hf)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : (fun x ↦ c) = (fun x ↦ c) ∘ X
b : β
⊢ (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b →
    (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : (fun x ↦ c) = (fun x ↦ c) ∘ X
b : β
hb : (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b
⊢ (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
⊢ IsMarkovKernel κ.condKernel

Tactic:
rw [condKernel_def]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
⊢ IsMarkovKernel (if hα : Countable α then condKernelCountable (fun a ↦ (κ a).condKernel) ⋯ else κ.condKernelBorel)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : (fun x ↦ c) = (fun x ↦ c) ∘ X
b : β
hb : (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b
⊢ (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
mβ : MeasurableSpace β
X : α → β
c : Ω
this : (fun x ↦ c) = (fun x ↦ c) ∘ X
b : β
hb : (condDistrib ((fun x ↦ c) ∘ X) X μ) b = (Kernel.deterministic (fun x ↦ c) ⋯) b
⊢ (Kernel.deterministic (fun x ↦ c) ⋯) b = (Kernel.deterministic (fun x ↦ c) ⋯) b
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
⊢ κ.fst ⊗ₖ κ.condKernel = κ

Tactic:
rw [condKernel_def]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : CountablyGenerated γ
mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
h : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
⊢ (κ.fst ⊗ₖ if hα : Countable α then condKernelCountable (fun a ↦ (κ a).condKernel) ⋯ else κ.condKernelBorel) = κ
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
by_cases hX : AEMeasurable X μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
by_cases hX : AEMeasurable X μ

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

case neg
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : ¬AEMeasurable X μ
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: case snd
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a : ι
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↑(Set.Ioi a)) → X ↑i)
i : ↑(Set.Ioi a)
⊢ ((fun x ↦ (fun i ↦ x ↑i, fun i ↦ x ↑i)) ((fun x i ↦ if hi : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩) x)).2 i = x.2 i

Tactic:
simp [not_le.2 <| Set.mem_Ioi.1 i.2]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b ↦ (a, b)) ⋯
h : ∀ᵐ (x : β) ∂(ρ a).fst, (κ.comap (fun b ↦ (a, b)) ⋯) x = (ρ a).condKernel x
b : β
⊢ (κ.comap (fun b ↦ (a, b)) ⋯) b = (ρ a).condKernel b → κ (a, b) = (ρ a).condKernel b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b ↦ (a, b)) ⋯
h : ∀ᵐ (x : β) ∂(ρ a).fst, (κ.comap (fun b ↦ (a, b)) ⋯) x = (ρ a).condKernel x
b : β
hb : (κ.comap (fun b ↦ (a, b)) ⋯) b = (ρ a).condKernel b
⊢ κ (a, b) = (ρ a).condKernel b
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[Measure.map Prod.fst ρ] ⇑ρ.condKernel
b : β
⊢ (Kernel.const α ρ).condKernel (a, b) = ρ.condKernel b → (Kernel.const α ρ).condKernel (a, b) = ρ.condKernel b

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
a : α
h : (fun b ↦ (Kernel.const α ρ).condKernel (a, b)) =ᵐ[Measure.map Prod.fst ρ] ⇑ρ.condKernel
b : β
hb : (Kernel.const α ρ).condKernel (a, b) = ρ.condKernel b
⊢ (Kernel.const α ρ).condKernel (a, b) = ρ.condKernel b
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[κ a] g a
a✝¹ : α
ha : f a✝¹ =ᵐ[κ a✝¹] g a✝¹
a✝ : β
⊢ f a✝¹ a✝ = g a✝¹ a✝ → f a✝¹ a✝ = g a✝¹ a✝

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᵐ[κ a] g a
a✝¹ : α
ha : f a✝¹ =ᵐ[κ a✝¹] g a✝¹
a✝ : β
hb : f a✝¹ a✝ = g a✝¹ a✝
⊢ f a✝¹ a✝ = g a✝¹ a✝
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : β → E
a : α
inst✝² : CompleteSpace E
g : α → β
inst✝¹ : MeasurableSingletonClass β
hg : Measurable g
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setIntegral_dirac f _ s]

Goal state after:
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0

Tactic:
by_cases hX : AEMeasurable X μ

Goal state after:
case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0

case neg
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : ¬AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0