awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h_1 : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ) atBot (𝓝 0)
h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0)
⊢ Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ENNReal.toReal 0))

Tactic:
exact h0.comp (h.comp hs_tendsto)

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h : Monotone s
hs_tendsto : Tendsto s atTop atTop
simp_rw : Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ρ.fst.real univ))
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mα ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) fun (c : α) ↦
        (preCDF ρ (s m) (a, c).2).toReal)
    atTop (𝓝 (Measure.real.{u_1} (α := α) (m := mα) ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) univ))

Tactic:
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]

Premises used: ProbabilityTheory.Kernel.const_apply, ProbabilityTheory.integral_preCDF_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) atTop
    (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)

Tactic:
have h := ρ.tendsto_IicSnd_atTop MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h_1 : Monotone s
hs_tendsto : Tendsto s atTop atTop
h :
  Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) atTop
    (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
⊢ Tendsto ENNReal.toReal (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ)) (𝓝 (ρ.fst.real univ))

Tactic:
have h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst.real univ)) :=
      ENNReal.continuousAt_toReal (measure_ne_top _ _)
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h_1 : Monotone s
hs_tendsto : Tendsto s atTop atTop
h :
  Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) atTop
    (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
h0 : Tendsto ENNReal.toReal (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ)) (𝓝 (ρ.fst.real univ))
⊢ Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ρ.fst.real univ))

Tactic:
h0.comp (h.comp hs_tendsto)

Premises used: MeasureTheory.Measure.real, ENNReal.toReal, Filter.Tendsto.comp, NNReal.toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h_1 : Monotone s
hs_tendsto : Tendsto s atTop atTop
h :
  Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) atTop
    (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
h0 : Tendsto ENNReal.toReal (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ)) (𝓝 (ρ.fst.real univ))
⊢ Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ρ.fst.real univ))

Tactic:
exact h0.comp (h.comp hs_tendsto)

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
rw :
  ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₁ : ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₂ : (ρ.IicSnd (↑q : ℝ)).real s = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₃ : ENNReal.toReal ((ρ.IicSnd (↑q : ℝ) : (a : Set α) → ℝ≥0∞) s) = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₄ :
  ENNReal.toReal ((ρ.IicSnd (↑q : ℝ) : (a : Set α) → ℝ≥0∞) s) =
    ENNReal.toReal ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))))
rw₅ rw₆ :
  ENNReal.toReal ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))) =
    ENNReal.toReal ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))))
⊢ (@integral _ _ _ _ mα (Measure.restrict ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) s) fun (c : α) ↦
      (preCDF ρ q (a, c).2).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))

Tactic:
rw [Kernel.const_apply, Kernel.const_apply,
    setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def, Measure.IicSnd_apply _ _ hs]

Premises used: MeasureTheory.Measure.IicSnd_apply, ProbabilityTheory.setIntegral_preCDF_fst, MeasureTheory.measureReal_def, ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ IsRatCondKernelCDF (mα := PUnit.instMeasurableSpace) (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal)
    (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

Tactic:
(isRatCondKernelCDFAux_preCDF ρ).isRatCondKernelCDF

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.isRatCondKernelCDF, ProbabilityTheory.isRatCondKernelCDFAux_preCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
h :
  ∀ (x : ℝ),
    (↑(condCDF ρ a) : ℝ → ℝ) x =
      (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x
⊢ condCDF ρ a = stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
h :
  (↑(stieltjesOfMeasurableRat (fun (a : α) (r : ℚ) ↦ (preCDF ρ r a).toReal) ⋯ a) : ℝ → ℝ) x =
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x
h₁ h₂ :
  (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x =
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x
⊢ (↑(condCDF ρ a) : ℝ → ℝ) x =
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x

Tactic:
rw [condCDF, ← stieltjesOfMeasurableRat_unit_prod]

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_unit_prod, ProbabilityTheory.condCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
simp_rw :
  IsCondKernelCDF (mα := PUnit.instMeasurableSpace)
    (fun (p : Unit × α) ↦ stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), p.2))
    (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
⊢ IsCondKernelCDF (mα := PUnit.instMeasurableSpace) (fun (p : Unit × α) ↦ condCDF ρ p.2) (Kernel.const Unit ρ)
    (Kernel.const Unit ρ.fst)

Tactic:
simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]

Premises used: ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (mα := PUnit.instMeasurableSpace)
    (fun (p : Unit × α) ↦ stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), p.2))
    (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

Tactic:
isCondKernelCDF_stieltjesOfMeasurableRat (isRatCondKernelCDF_preCDF ρ)

Premises used: ProbabilityTheory.isRatCondKernelCDF_preCDF, ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (mα := PUnit.instMeasurableSpace)
    (fun (p : Unit × α) ↦ stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), p.2))
    (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

Tactic:
exact isCondKernelCDF_stieltjesOfMeasurableRat (isRatCondKernelCDF_preCDF ρ)

Premises used: ProbabilityTheory.isRatCondKernelCDF_preCDF, ProbabilityTheory.isCondKernelCDF_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
r : ℝ
⊢ 0 ≤ (↑(condCDF ρ a) : ℝ → ℝ) r

Tactic:
stieltjesOfMeasurableRat_nonneg _ a r

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ (↑(condCDF ρ a) : ℝ → ℝ) x ≤ 1

Tactic:
stieltjesOfMeasurableRat_le_one _ _ _

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ Tendsto (↑(condCDF ρ a) : ℝ → ℝ) atBot (𝓝 0)

Tactic:
tendsto_stieltjesOfMeasurableRat_atBot _ _

Premises used: ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atBot
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ Tendsto (↑(condCDF ρ a) : ℝ → ℝ) atTop (𝓝 1)

Tactic:
tendsto_stieltjesOfMeasurableRat_atTop _ _

Premises used: ProbabilityTheory.tendsto_stieltjesOfMeasurableRat_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
simp_rw :
  (ae ρ.fst).EventuallyEq (β := ℝ)
    (fun (a : α) ↦
      (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) (↑r : ℝ))
    fun (a : α) ↦ (preCDF ρ r a).toReal
⊢ (ae ρ.fst).EventuallyEq (β := ℝ) (fun (a : α) ↦ (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ)) fun (a : α) ↦ (preCDF ρ r a).toReal

Tactic:
simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]

Premises used: ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
⊢ (ae ρ.fst).EventuallyEq (β := ℝ)
    (fun (a : α) ↦
      (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) (↑r : ℝ))
    fun (a : α) ↦ (preCDF ρ r a).toReal

Tactic:
stieltjesOfMeasurableRat_ae_eq (isRatCondKernelCDF_preCDF ρ) () r

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, Unit.unit, ProbabilityTheory.isRatCondKernelCDF_preCDF, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
⊢ (ae ρ.fst).EventuallyEq (β := ℝ)
    (fun (a : α) ↦
      (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) (↑r : ℝ))
    fun (a : α) ↦ (preCDF ρ r a).toReal

Tactic:
exact stieltjesOfMeasurableRat_ae_eq (isRatCondKernelCDF_preCDF ρ) () r

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, Unit.unit, ProbabilityTheory.isRatCondKernelCDF_preCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
h :
  ∀ (a : α) (ha : (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ) = (preCDF ρ r a).toReal) (ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1),
    ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ)) = preCDF ρ r a
⊢ (fun (a : α) ↦ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ))) =ᶠ[ae ρ.fst] preCDF ρ r

Tactic:
filter_upwards [condCDF_ae_eq ρ r, preCDF_le_one ρ] with a ha ha_le_one

Premises used: ProbabilityTheory.condCDF_ae_eq, ProbabilityTheory.preCDF_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
a : α
ha : (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ) = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
h : preCDF ρ r a ≠ ∞
⊢ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ)) = preCDF ρ r a

Tactic:
rw [ha, ENNReal.ofReal_toReal]

Premises used: ENNReal.ofReal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
a : α
ha : (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ) = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a ≠ ∞

Tactic:
((ha_le_one r).trans_lt ENNReal.one_lt_top).ne

Premises used: ENNReal.one_lt_top, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
a : α
ha : (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ) = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a ≠ ∞

Tactic:
exact ((ha_le_one r).trans_lt ENNReal.one_lt_top).ne

Premises used: ENNReal.one_lt_top, LE.le.trans_lt, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
x : ℝ
⊢ Measurable (β := ℝ) fun (a : α) ↦ (↑(condCDF ρ a) : ℝ → ℝ) x

Tactic:
measurable_stieltjesOfMeasurableRat _ _

Premises used: ProbabilityTheory.measurable_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
x : ℝ
⊢ StronglyMeasurable (β := ℝ) fun (a : α) ↦ (↑(condCDF ρ a) : ℝ → ℝ) x

Tactic:
stronglyMeasurable_stieltjesOfMeasurableRat _ _

Premises used: ProbabilityTheory.stronglyMeasurable_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℝ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x) ∂ρ.fst = (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
(isCondKernelCDF_condCDF ρ).setLIntegral () hs x

Premises used: Unit.unit, ProbabilityTheory.IsCondKernelCDF.setLIntegral, ProbabilityTheory.isCondKernelCDF_condCDF, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℝ
⊢ ∫⁻ (a : α), ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x) ∂ρ.fst =
    (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (α := Set α) univ (Iic x))

Tactic:
(isCondKernelCDF_condCDF ρ).lintegral () x

Premises used: Unit.unit, ProbabilityTheory.isCondKernelCDF_condCDF, ProbabilityTheory.IsCondKernelCDF.lintegral, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℝ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (↑(condCDF ρ a) : ℝ → ℝ) x) ρ.fst

Tactic:
(isCondKernelCDF_condCDF ρ).integrable () x

Premises used: Unit.unit, ProbabilityTheory.IsCondKernelCDF.integrable, ProbabilityTheory.isCondKernelCDF_condCDF, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℝ
s : Set α
hs : MeasurableSet s
⊢ ∫ (a : α) in s, (↑(condCDF ρ a) : ℝ → ℝ) x ∂ρ.fst = ρ.real (s ×ˢ Iic x)

Tactic:
(isCondKernelCDF_condCDF ρ).setIntegral () hs x

Premises used: Unit.unit, ProbabilityTheory.IsCondKernelCDF.setIntegral, ProbabilityTheory.isCondKernelCDF_condCDF, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℝ
⊢ ∫ (a : α), (↑(condCDF ρ a) : ℝ → ℝ) x ∂ρ.fst = ρ.real (SProd.sprod (α := Set α) univ (Iic x))

Tactic:
(isCondKernelCDF_condCDF ρ).integral () x

Premises used: Unit.unit, ProbabilityTheory.IsCondKernelCDF.integral, ProbabilityTheory.isCondKernelCDF_condCDF, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
rw : ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) = ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x - 0)
⊢ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) = ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x)

Tactic:
rw [← sub_zero (condCDF ρ a x)]

Premises used: sub_zero, StieltjesFunction.toFun, ProbabilityTheory.condCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) = ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x - 0)

Tactic:
(condCDF ρ a).measure_Iic (tendsto_condCDF_atBot ρ a) _

Premises used: ProbabilityTheory.tendsto_condCDF_atBot, StieltjesFunction.measure_Iic, ProbabilityTheory.condCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) = ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x - 0)

Tactic:
exact (condCDF ρ a).measure_Iic (tendsto_condCDF_atBot ρ a) _

Premises used: ProbabilityTheory.tendsto_condCDF_atBot, StieltjesFunction.measure_Iic, ProbabilityTheory.condCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
rw : ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)
⊢ Eq (α := ℝ≥0∞) (((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]

Premises used: sub_zero, ENNReal.ofReal_one, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)

Tactic:
StieltjesFunction.measure_univ _ (tendsto_condCDF_atBot ρ a) (tendsto_condCDF_atTop ρ a)

Premises used: ProbabilityTheory.tendsto_condCDF_atBot, StieltjesFunction.measure_univ, ProbabilityTheory.tendsto_condCDF_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)

Tactic:
exact StieltjesFunction.measure_univ _ (tendsto_condCDF_atBot ρ a) (tendsto_condCDF_atTop ρ a)

Premises used: ProbabilityTheory.tendsto_condCDF_atBot, StieltjesFunction.measure_univ, ProbabilityTheory.tendsto_condCDF_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ IsProbabilityMeasure (m0 := Real.measurableSpace) (condCDF ρ a).measure

Tactic:
⟨measure_condCDF_univ ρ a⟩

Premises used: MeasureTheory.IsProbabilityMeasure.mk, ProbabilityTheory.measure_condCDF_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
simp_rw : ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) i)
⊢ ∀ (s : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (range Iic) s →
      Measurable (β := ℝ≥0∞) fun (a : α) ↦ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) s

Tactic:
simp_rw [forall_mem_range, measure_condCDF_Iic]

Premises used: Set.forall_mem_range, ProbabilityTheory.measure_condCDF_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) i)

Tactic:
fun u ↦ (measurable_condCDF ρ u).ennreal_ofReal

Premises used: Measurable.ennreal_ofReal, ProbabilityTheory.measurable_condCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) i)

Tactic:
exact fun u ↦ (measurable_condCDF ρ u).ennreal_ofReal

Premises used: Measurable.ennreal_ofReal, ProbabilityTheory.measurable_condCDF
-- 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 α γ
n : ℕ
a : α
s : Set β
⊢ Eq.{u_3 + 1} (α := (t : γ) → ℝ) (fun (t : γ) ↦ κ.densityProcess ν n a t s) fun (t : γ) ↦
    (HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
            (countablePartitionSet n t ×ˢ s) :
          ℝ≥0∞)
        ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n t) : ℝ≥0∞)).toReal

Tactic:
rfl

Premises used: ProbabilityTheory.Kernel.densityProcess, rfl
-- 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 α γ
n : ℕ
s : Set β
hs : MeasurableSet s
change :
  Measurable (α := α × γ) (β := ℝ≥0∞)
    ((fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
        HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
            ℝ≥0∞)
          ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)) ∘
      fun (p : α × γ) ↦
      (p.1, Subtype.mk (p := fun (x : Set γ) ↦ x ∈ countablePartition γ n) (countablePartitionSet n p.2) ⋯))
⊢ Measurable (β := ℝ≥0∞) fun (p : α × γ) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n p.2 ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n p.2) : ℝ≥0∞)

Tactic:
change Measurable[mα.prod (countableFiltration γ n)]
      ((fun (p : α × countablePartition γ n) ↦ κ p.1 (↑p.2 ×ˢ s) / ν p.1 p.2)
        ∘ (fun (p : α × γ) ↦ (p.1, ⟨countablePartitionSet n p.2, countablePartitionSet_mem n p.2⟩)))

Premises used: SProd.sprod, Measurable, MeasurableSpace.countablePartitionSet, Function.comp, HDiv.hDiv, Prod.mk, Prod.fst, Subtype.mk, MeasurableSpace.countablePartitionSet_mem, Subtype.val, Prod.snd, DFunLike.coe
-- 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 α γ
n : ℕ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (p : Prod.{u_1, u_3} α (↑(countablePartition γ n) : Type u_3)) ↦
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) p.1 : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) ((↑p.2 : Set γ) ×ˢ s) :
        ℝ≥0∞)
      ((((ν : (a : α) → Measure γ) p.1 : Measure γ) : (a : Set γ) → ℝ≥0∞) (↑p.2 : Set γ) : ℝ≥0∞)

Tactic:
Measurable.div ?_ ?_

Premises used: Measurable.div