awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
compl :
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
compl₁ : A ⊆ univ
⊢ ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)) ≤
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s))

Tactic:
gcongr
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
⊢ Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ s) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A_1 : Set γ
this_1 : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
A : Set γ
hA : MeasurableSet A
hA_eq :
  (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)
h :
  (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s) +
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) Aᶜ) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (SProd.sprod (α := Set γ) univ s)
this : Aᶜ ×ˢ s = SProd.sprod (α := Set γ) univ s \ A ×ˢ s
⊢ A ⊆ univ

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
iUnion :
  (∑' (n : ℕ),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f n)) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s)
⊢ (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (⋃ (i : ℕ), f i)) fun (x : γ) ↦
      κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s)

Tactic:
rw [integral_iUnion hf hf_disj (integrable_density hκν _ hs).integrableOn]

Premises used: ProbabilityTheory.Kernel.integrable_density, MeasureTheory.Integrable.integrableOn, MeasureTheory.integral_iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
iUnion :
  ∑' (n : ℕ),
      ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (f n ×ˢ s)) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s))
⊢ (∑' (n : ℕ),
      @integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f n)) fun (x : γ) ↦ κ.density ν a x s) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s)

Tactic:
simp_rw [h_eq, measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
iUnion :
  ENNReal.toReal
      (∑' (a_1 : ℕ), (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (f a_1 ×ˢ s)) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s))
⊢ ∑' (n : ℕ),
      ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (f n ×ˢ s)) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s))

Tactic:
rw [← ENNReal.tsum_toReal_eq (fun _ ↦ measure_ne_top _ _)]

Premises used: MeasureTheory.measure_ne_top, ENNReal.tsum_toReal_eq
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
iUnion :
  Eq (α := ℝ≥0∞)
    (∑' (a_1 : ℕ), (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (f a_1 ×ˢ s) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s) :
      ℝ≥0∞)
⊢ ENNReal.toReal
      (∑' (a_1 : ℕ), (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (f a_1 ×ˢ s)) =
    ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s))

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
iUnion : Pairwise (α := ℕ) (Function.onFun (β := Set (γ × β)) Disjoint fun (i : ℕ) ↦ f i ×ˢ s)
iUnion₁ : ∀ (i : ℕ), MeasurableSet (f i ×ˢ s)
⊢ Eq (α := ℝ≥0∞)
    (∑' (a_1 : ℕ), (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (f a_1 ×ˢ s) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) (⋃ (i : ℕ), f i) s) :
      ℝ≥0∞)

Tactic:
rw [iUnion_prod_const, measure_iUnion]

Premises used: Set.iUnion_prod_const, MeasureTheory.measure_iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
⊢ Pairwise (α := ℕ) (Function.onFun (β := Set (γ × β)) Disjoint fun (i : ℕ) ↦ f i ×ˢ s)

Tactic:
hf_disj.mono fun _ _ h ↦ h.set_prod_left _ _

Premises used: Set.Disjoint.set_prod_left, Pairwise.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
⊢ Pairwise (α := ℕ) (Function.onFun (β := Set (γ × β)) Disjoint fun (i : ℕ) ↦ f i ×ˢ s)

Tactic:
exact hf_disj.mono fun _ _ h ↦ h.set_prod_left _ _

Premises used: Set.Disjoint.set_prod_left, Pairwise.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
⊢ ∀ (i : ℕ), MeasurableSet (f i ×ˢ s)

Tactic:
fun i ↦ (hf i).prod hs

Premises used: MeasurableSet.prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
this : IsFiniteKernel κ
hgen : mγ = generateFrom {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
hpi : IsPiSystem.{u_3} (α := γ) {s : Set γ | ∃ (n : ℕ), MeasurableSet s}
f : ℕ → Set γ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
h_eq :
  ∀ (i : ℕ),
    (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) (f i)) fun (x : γ) ↦ κ.density ν a x s) =
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (f i ×ˢ s)
⊢ ∀ (i : ℕ), MeasurableSet (f i ×ˢ s)

Tactic:
exact fun i ↦ (hf i).prod hs

Premises used: MeasurableSet.prod
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)
hfi : @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x s) (Measure.restrict ((ν : (a : α) → Measure γ) a) A)
f_nn :
  (ae (F := Measure γ) (Measure.restrict ((ν : (a : α) → Measure γ) a) A)).EventuallyLE (β := ℝ) 0 fun (x : γ) ↦
    κ.density ν a x s
⊢ ∫⁻ (x : γ) in A, ENNReal.ofReal (κ.density ν a x s) ∂(ν : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
rw :
  ENNReal.ofReal (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) (A ×ˢ s)) =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)
rw₁ :
  ENNReal.ofReal
      (ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s))) =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s) : ℝ≥0∞)
⊢ ENNReal.ofReal
      (@integral _ _ _ _ mγ (Measure.restrict ((ν : (a : α) → Measure γ) a) A) fun (x : γ) ↦ κ.density ν a x s) =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (A ×ˢ s)

Tactic:
rw [setIntegral_density hκν a hs hA, measureReal_def,
      ENNReal.ofReal_toReal (measure_ne_top _ _)]

Premises used: MeasureTheory.measure_ne_top, ENNReal.ofReal_toReal, MeasureTheory.measureReal_def, ProbabilityTheory.Kernel.setIntegral_density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x s) (Measure.restrict ((ν : (a : α) → Measure γ) a) A)

Tactic:
(integrable_density hκν a hs).restrict

Premises used: MeasureTheory.Integrable.restrict, ProbabilityTheory.Kernel.integrable_density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x s) (Measure.restrict ((ν : (a : α) → Measure γ) a) A)

Tactic:
exact (integrable_density hκν a hs).restrict

Premises used: MeasureTheory.Integrable.restrict, ProbabilityTheory.Kernel.integrable_density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ (ae (F := Measure γ) (Measure.restrict ((ν : (a : α) → Measure γ) a) A)).EventuallyLE (β := ℝ) 0 fun (x : γ) ↦
    κ.density ν a x s

Tactic:
ae_of_all _ (fun _ ↦ density_nonneg hκν _ _ _)

Premises used: MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.density_nonneg, Filter.EventuallyLE
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : IsFiniteKernel κ
⊢ (ae (F := Measure γ) (Measure.restrict ((ν : (a : α) → Measure γ) a) A)).EventuallyLE (β := ℝ) 0 fun (x : γ) ↦
    κ.density ν a x s

Tactic:
exact ae_of_all _ (fun _ ↦ density_nonneg hκν _ _ _)

Premises used: MeasureTheory.ae_of_all, ProbabilityTheory.Kernel.density_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
rw :
  ∫⁻ (x : γ) in univ, ENNReal.ofReal (κ.density ν a x s) ∂(ν : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (SProd.sprod (α := Set γ) univ s)
⊢ ∫⁻ (x : γ), ENNReal.ofReal (κ.density ν a x s) ∂(ν : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (SProd.sprod (α := Set γ) univ s)

Tactic:
rw [← setLIntegral_univ]

Premises used: MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in univ, ENNReal.ofReal (κ.density ν a x s) ∂(ν : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (SProd.sprod (α := Set γ) univ s)

Tactic:
setLIntegral_density hκν a hs MeasurableSet.univ

Premises used: ProbabilityTheory.Kernel.setLIntegral_density, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in univ, ENNReal.ofReal (κ.density ν a x s) ∂(ν : (a : α) → Measure γ) a =
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) (SProd.sprod (α := Set γ) univ s)

Tactic:
exact setLIntegral_density hκν a hs MeasurableSet.univ

Premises used: ProbabilityTheory.Kernel.setLIntegral_density, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ IsFiniteKernel κ

Tactic:
have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)