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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
⊢ ∀ (i : ℚ),
    ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β),
      ⨅ (r : (↑(Ioi i) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) i

Tactic:
fun q ↦ ae_eq_of_forall_setIntegral_eq_of_sigmaFinite (μ := ν a) ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite, Filter.EventuallyEq
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
refine_1 :
  ∀ (q : ℚ) (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, a_3) (↑r : ℚ)) s
          ((ν : (a : α) → Measure β) a)
refine_2 :
  ∀ (q : ℚ) (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ f (a, a_3) q) s ((ν : (a : α) → Measure β) a)
refine_3 :
  ∀ (q : ℚ) (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ)
          (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
            ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ))
          (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦ f (a, x) q)
⊢ ∀ (i : ℚ),
    ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β),
      ⨅ (r : (↑(Ioi i) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) i

Tactic:
refine fun q ↦ ae_eq_of_forall_setIntegral_eq_of_sigmaFinite (μ := ν a) ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, a_3) (↑r : ℚ)) s
          ((ν : (a : α) → Measure β) a)

Tactic:
fun _ _ _ ↦ (hf.integrable_iInf_rat_gt _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ ⨅ (r : (↑(Ioi q) : Type)), f (a, a_3) (↑r : ℚ)) s
          ((ν : (a : α) → Measure β) a)

Tactic:
exact fun _ _ _ ↦ (hf.integrable_iInf_rat_gt _ _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ f (a, a_3) q) s ((ν : (a : α) → Measure β) a)

Tactic:
fun _ _ _ ↦ (hf.integrable a _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
⊢ ∀ (s : Set β),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ) (mα := mβ) (fun (a_3 : β) ↦ f (a, a_3) q) s ((ν : (a : α) → Measure β) a)

Tactic:
exact fun _ _ _ ↦ (hf.integrable a _).integrableOn

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
refine_3 :
  LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ)
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ))
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦ f (a, x) q)
⊢ LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ)
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ))
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦ f (a, x) q)

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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
refine_3₁ refine_3₂ :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ))
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦ f (a, x) q)

Tactic:
rw [hf.setIntegral _ hs, hf.setIntegral_iInf_rat_gt _ _ hs]

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
h :
  ∀ (t : β) (ht_top : Tendsto (f (a, t)) atTop (𝓝 1)) (ht_bot : Tendsto (f (a, t)) atBot (𝓝 0))
    (ht_iInf : ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ) = f (a, t) q) (h_mono : Monotone (f (a, t))),
    IsRatStieltjesPoint f (a, t)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), IsRatStieltjesPoint f (a, t)

Tactic:
filter_upwards [hf.tendsto_atTop_one a, hf.tendsto_atBot_zero a,
    hf.iInf_rat_gt_eq a, hf.mono a] with t ht_top ht_bot ht_iInf h_mono

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero, ProbabilityTheory.IsRatCondKernelCDFAux.mono, ProbabilityTheory.IsRatCondKernelCDFAux.iInf_rat_gt_eq, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atTop_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
t : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)
ht_iInf : ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ) = f (a, t) q
h_mono : Monotone (f (a, t))
⊢ IsRatStieltjesPoint f (a, t)

Tactic:
⟨h_mono, ht_top, ht_bot, ht_iInf⟩

Premises used: ProbabilityTheory.IsRatStieltjesPoint.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
t : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)
ht_iInf : ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ) = f (a, t) q
h_mono : Monotone (f (a, t))
⊢ IsRatStieltjesPoint f (a, t)

Tactic:
exact ⟨h_mono, ht_top, ht_bot, ht_iInf⟩
-- 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 ℝ
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ 0 ≤ (↑(f p) : ℝ → ℝ) x

Tactic:
Monotone.le_of_tendsto (f p).mono (hf.tendsto_atBot_zero p) x

Premises used: StieltjesFunction.mono, ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero, Monotone.le_of_tendsto
-- 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 ℝ
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ (↑(f p) : ℝ → ℝ) x ≤ 1

Tactic:
Monotone.ge_of_tendsto (f p).mono (hf.tendsto_atTop_one p) x

Premises used: ProbabilityTheory.IsCondKernelCDF.tendsto_atTop_one, Monotone.ge_of_tendsto, StieltjesFunction.mono
-- 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 ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
rw :
  Eq (α := ℝ) (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x)
    (@MeasureTheory.integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) univ) fun (b : β) ↦
      (↑(f (a, b)) : ℝ → ℝ) x)
rw₁ rw₂ :
  Eq (α := ℝ) (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x)
    (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x)
⊢ (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))

Tactic:
rw [← hf.setIntegral _ MeasurableSet.univ, Measure.restrict_univ]

Premises used: ProbabilityTheory.IsCondKernelCDF.setIntegral, MeasurableSet.univ, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
inst : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
x : ℝ
rw :
  ENNReal.ofReal
      (@MeasureTheory.integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x_1 : β) ↦
        (↑(f (a, x_1)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
rw₁ :
  ENNReal.ofReal (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (hf.integrable a x).restrict
    (ae_of_all _ (fun _ ↦ hf.nonneg _ _)), hf.setIntegral a hs x, ofReal_measureReal]

Premises used: ProbabilityTheory.IsCondKernelCDF.nonneg, MeasureTheory.ofReal_measureReal, MeasureTheory.Integrable.restrict, ProbabilityTheory.IsCondKernelCDF.setIntegral, Prod.mk, ProbabilityTheory.IsCondKernelCDF.integrable, MeasureTheory.ae_of_all, MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
inst : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
rw :
  ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in univ, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a
rw₁ rw₂ :
  ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x))

Tactic:
rw [← hf.setLIntegral _ MeasurableSet.univ, Measure.restrict_univ]

Premises used: ProbabilityTheory.IsCondKernelCDF.setLIntegral, MeasurableSet.univ, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
⊢ Eq (α := Measure ℝ) ((toKernel f hf : (a : α × β) → Measure ℝ) p : Measure ℝ) ((f p).measure : Measure ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ_1 : Kernel.{u_1, u_2} α (β × ℝ)
ν_1 : Kernel α β
x : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
⊢ IsMarkovKernel (IsCondKernelCDF.toKernel f hf)

Tactic:
⟨fun _ ↦ (f _).isProbabilityMeasure (hf.tendsto_atBot_zero _) (hf.tendsto_atTop_one _)⟩

Premises used: ProbabilityTheory.IsCondKernelCDF.tendsto_atTop_one, StieltjesFunction.isProbabilityMeasure, ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x_1 : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
rw : ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x - 0) = ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x)
⊢ (((toKernel f hf : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x)

Tactic:
rw [IsCondKernelCDF.toKernel_apply p, (f p).measure_Iic (hf.tendsto_atBot_zero p)]

Premises used: ProbabilityTheory.IsCondKernelCDF.tendsto_atBot_zero, StieltjesFunction.measure_Iic, ProbabilityTheory.IsCondKernelCDF.toKernel_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x_1 : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x - 0) = ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x)

Tactic:
simp
-- 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 : α
x : ℝ
s : Set β
hs : MeasurableSet s
simp_rw :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
simp_rw [IsCondKernelCDF.toKernel_Iic]

Premises used: ProbabilityTheory.IsCondKernelCDF.toKernel_Iic
-- 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 : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
hf.setLIntegral _ hs _

Premises used: ProbabilityTheory.IsCondKernelCDF.setLIntegral
-- 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 : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
exact hf.setLIntegral _ hs _

Premises used: ProbabilityTheory.IsCondKernelCDF.setLIntegral
-- 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 β
hs : MeasurableSet s
rw :
  ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (r : ℚ), Iic (↑r : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        univ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s univ)

Tactic:
rw [← Real.iUnion_Iic_rat, prod_iUnion]

Premises used: Real.iUnion_Iic_rat, Set.prod_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 κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
⊢ Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)

Tactic:
Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_

Premises used: Iff.mpr, Set.Iic_subset_Iic, Monotone.directed_le
-- 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 β
hs : MeasurableSet s
refine : ∀ (r r' : ℚ) (hrr' : r ≤ r'), LE.le (α := ℝ) (↑r : ℝ) (↑r' : ℝ)
⊢ Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)

Tactic:
refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_

Premises used: Iff.mpr, Set.Iic_subset_Iic, Monotone.directed_le
-- 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 β
hs : MeasurableSet s
r r' : ℚ
hrr' : r ≤ r'
⊢ LE.le (α := ℝ) (↑r : ℝ) (↑r' : ℝ)

Tactic:
mod_cast hrr'

Premises used: cast, Eq.symm, Rat.cast_le._simp_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 β
hs : MeasurableSet s
r r' : ℚ
hrr' : r ≤ r'
⊢ LE.le (α := ℝ) (↑r : ℝ) (↑r' : ℝ)

Tactic:
exact mod_cast hrr'
-- 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 β
hs : MeasurableSet s
⊢ Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)

Tactic:
have h_dir : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ Iic (q : ℝ) := by
    refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_
    exact mod_cast hrr'
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
⊢ Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))

Tactic:
Monotone.directed_le fun i j hij ↦ ?_

Premises used: Monotone.directed_le
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
refine :
  ∀ (i j : ℚ) (hij : i ≤ j), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)) ≤ SProd.sprod (β := Set ℝ) s (Iic (↑j : ℝ))
⊢ Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))

Tactic:
refine Monotone.directed_le fun i j hij ↦ ?_

Premises used: Monotone.directed_le