awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
a_1 : β
i : ℕ
_ : ∀ ⦃j : ℕ⦄, i ≠ j → Function.onFun (β := Set ℝ) Disjoint (fun (i : ℕ) ↦ Prod.mk a_1 ⁻¹' f' i) i j
⊢ ∀ ⦃j : ℕ⦄, i ≠ j → Function.onFun (β := Set ℝ) Disjoint (fun (i : ℕ) ↦ Prod.mk a_1 ⁻¹' f' i) i j

Tactic:
_
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
a_1 : β
i j : ℕ
hij : i ≠ j
⊢ Function.onFun (β := Set ℝ) Disjoint (fun (i : ℕ) ↦ Prod.mk a_1 ⁻¹' f' i) i j

Tactic:
Disjoint.preimage _ (hf_disj hij)

Premises used: Disjoint.preimage
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
a_1 : β
i j : ℕ
hij : i ≠ j
⊢ Function.onFun (β := Set ℝ) Disjoint (fun (i : ℕ) ↦ Prod.mk a_1 ⁻¹' f' i) i j

Tactic:
exact Disjoint.preimage _ (hf_disj hij)

Premises used: Disjoint.preimage
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
⊢ ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)

Tactic:
have h_disj : ∀ a, Pairwise (Disjoint on fun i ↦ Prod.mk a ⁻¹' f' i) := by
      intro _ _ _ hij
      exact Disjoint.preimage _ (hf_disj hij)
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
e_f :
  ∀ (x : β),
    Eq (α := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (⋃ (i : ℕ), Prod.mk x ⁻¹' f' i) :
        ℝ≥0∞)
      (∑' (i : ℕ),
          (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk x ⁻¹' f' i) :
        ℝ≥0∞)
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a

Tactic:
congr with x : 1
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
x : β
e_f e_f₁ :
  Eq (α := ℝ≥0∞)
    (∑' (i : ℕ),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' f' i))
    (∑' (i : ℕ),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' f' i))
⊢ Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk x ⁻¹' f' i) :
      ℝ≥0∞)
    (∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' f' i) :
      ℝ≥0∞)

Tactic:
rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]

Premises used: MeasureTheory.measure_iUnion, measurable_prodMk_left
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
⊢ ∫⁻ (b : β),
      ∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    ∑' (i : ℕ),
      ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a

Tactic:
lintegral_tsum fun i ↦ (Kernel.measurable_kernel_prodMk_left' (hf_meas i) a).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', MeasureTheory.lintegral_tsum
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a)
    (∑' (i : ℕ), (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i))

Tactic:
simp_rw [hf_eq]
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : ℕ), (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (iUnion f') : ℝ≥0∞)

Tactic:
(measure_iUnion hf_disj hf_meas).symm

Premises used: MeasureTheory.measure_iUnion, Eq.symm
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
f' : ℕ → Set (β × ℝ)
hf_disj : Pairwise (Disjoint on f')
hf_meas : ∀ (i : ℕ), MeasurableSet (f' i)
hf_eq :
  ∀ (i : ℕ),
    ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i)
h_eq : ∀ (a : β), Eq (α := Set ℝ) (Prod.mk a ⁻¹' ⋃ (i : ℕ), f' i) (⋃ (i : ℕ), Prod.mk a ⁻¹' f' i)
h_disj : ∀ (a : β), Pairwise (α := ℕ) (Function.onFun (β := Set ℝ) Disjoint fun (i : ℕ) ↦ Prod.mk a ⁻¹' f' i)
calc :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      ∑' (i : ℕ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a
calc₁ :
  Eq (α := ℝ≥0∞)
    (∑' (i : ℕ),
      ∫⁻ (b : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a)
    (∑' (i : ℕ), (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (f' i))
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i : ℕ), Prod.mk b ⁻¹' f' i) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (⋃ (i : ℕ), f' i)

Tactic:
calc ∫⁻ b, hf.toKernel f (a, b) (⋃ i, Prod.mk b ⁻¹' f' i) ∂(ν a)
      = ∫⁻ b, ∑' i, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) := by
          congr with x : 1
          rw [measure_iUnion (h_disj x) fun i ↦ measurable_prodMk_left (hf_meas i)]
    _ = ∑' i, ∫⁻ b, hf.toKernel f (a, b) (Prod.mk b ⁻¹' f' i) ∂(ν a) :=
          lintegral_tsum fun i ↦ (Kernel.measurable_kernel_prodMk_left' (hf_meas i) a).aemeasurable
    _ = ∑' i, κ a (f' i) := by simp_rw [hf_eq]
    _ = κ a (iUnion f') := (measure_iUnion hf_disj hf_meas).symm

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.measurable_kernel_prodMk_left', MeasureTheory.measure_iUnion, Eq.symm, MeasureTheory.lintegral_tsum, DFunLike.coe, Set.iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
inst_1 : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
h :
  ∀ (a : α) (s : Set (β × ℝ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((ν ⊗ₖ IsCondKernelCDF.toKernel f hf : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) :
            (a : Set (β × ℝ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ν ⊗ₖ IsCondKernelCDF.toKernel f hf = κ

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
inst_1 : IsSFiniteKernel ν
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
hs : MeasurableSet s
h :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' s) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s
h₁ h₂ :
  Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((ν ⊗ₖ IsCondKernelCDF.toKernel f hf : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Kernel.compProd_apply hs, lintegral_toKernel_mem hf a hs]

Premises used: ProbabilityTheory.lintegral_toKernel_mem, ProbabilityTheory.Kernel.compProd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r))).fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ρ.restrict (SProd.sprod (α := Set α) univ (Iic r)) : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ SProd.sprod (α := Set α) univ (Iic r)) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₃ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)
rw₄ rw₅ :
  Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' Iic r) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ρ.IicSnd r : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic r) : ℝ≥0∞)

Tactic:
rw [IicSnd, fst_apply hs, restrict_apply' (MeasurableSet.univ.prod measurableSet_Iic),
    univ_prod, Set.prod_eq]

Premises used: MeasureTheory.Measure.IicSnd, Set.univ_prod, MeasurableSet.prod, measurableSet_Iic, Set.prod_eq, MeasureTheory.Measure.fst_apply, MeasureTheory.Measure.restrict_apply', MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
⊢ Eq (α := ℝ≥0∞) ((ρ.IicSnd r : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ (Iic r)) : ℝ≥0∞)

Tactic:
IicSnd_apply ρ r MeasurableSet.univ

Premises used: MeasureTheory.Measure.IicSnd_apply, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r r' : ℝ
h_le : r ≤ r'
⊢ (ρ.restrict (SProd.sprod (α := Set α) univ (Iic r))).fst ≤ (ρ.restrict (SProd.sprod (α := Set α) univ (Iic r'))).fst

Tactic:
gcongr
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
⊢ ρ.IicSnd r ≤ ρ.fst

Tactic:
fst_mono restrict_le_self

Premises used: MeasureTheory.Measure.fst_mono, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℝ
⊢ ρ.IicSnd r ≪ ρ.fst

Tactic:
Measure.absolutelyContinuous_of_le (IicSnd_le_fst ρ r)

Premises used: MeasureTheory.Measure.IicSnd_le_fst, MeasureTheory.Measure.absolutelyContinuous_of_le
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℝ
⊢ IsFiniteMeasure (ρ.IicSnd r)

Tactic:
isFiniteMeasure_of_le _ (IicSnd_le_fst ρ _)

Premises used: MeasureTheory.isFiniteMeasure_of_le, MeasureTheory.Measure.IicSnd_le_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
t : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
simp_rw :
  Eq (α := ℝ≥0∞)
    (⨅ (r : { r' : ℚ // t < r' }), (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(↑r : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑t : ℝ))) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨅ (r : { r' : ℚ // t < r' }), (ρ.IicSnd (↑(↑r : ℚ) : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ.IicSnd (↑t : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [ρ.IicSnd_apply _ hs, Measure.iInf_rat_gt_prod_Iic hs]

Premises used: MeasureTheory.Measure.IicSnd_apply, MeasureTheory.Measure.iInf_rat_gt_prod_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
simp_rw :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s univ)) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
simp_rw [ρ.IicSnd_apply _ hs, fst_apply hs, ← prod_univ]

Premises used: Set.prod_univ, MeasureTheory.Measure.fst_apply, MeasureTheory.Measure.IicSnd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
rw :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s univ)) : Filter ℝ≥0∞)

Tactic:
rw [← Real.iUnion_Iic_rat, prod_iUnion]

Premises used: Real.iUnion_Iic_rat, Set.prod_iUnion
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
hm : Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)

Tactic:
apply tendsto_measure_iUnion_atTop

Premises used: MeasureTheory.tendsto_measure_iUnion_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))

Tactic:
monotone_const.set_prod Rat.cast_mono.Iic

Premises used: monotone_const, Monotone.set_prod, Rat.cast_mono, Monotone.Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))

Tactic:
exact monotone_const.set_prod Rat.cast_mono.Iic

Premises used: monotone_const, Monotone.set_prod, Rat.cast_mono, Monotone.Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
simp_rw :
  Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) atBot
    (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s) atBot (𝓝 0)

Tactic:
simp_rw [ρ.IicSnd_apply _ hs]

Premises used: MeasureTheory.Measure.IicSnd_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [prod_empty, measure_empty]

Premises used: MeasureTheory.measure_empty, Set.prod_empty
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have h_empty : ρ (s ×ˢ ∅) = 0 := by simp only [prod_empty, measure_empty]