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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal

Tactic:
have : (fun b ↦ stieltjesOfMeasurableRat f hf.measurable (a, b) x)
      = fun b ↦ (ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x)).toReal := by
    ext t
    rw [ENNReal.toReal_ofReal]
    exact stieltjesOfMeasurableRat_nonneg _ _ _
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
rw :
  @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal)
    ((ν : (a : α) → Measure β) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
    ((ν : (a : α) → Measure β) a)

Tactic:
rw [this]
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal)
    ((ν : (a : α) → Measure β) a)

Tactic:
integrable_toReal_of_lintegral_ne_top ?_ ?_

Premises used: MeasureTheory.integrable_toReal_of_lintegral_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
refine_1 :
  AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)) ((ν : (a : α) → Measure β) a)
refine_2 :
  ∫⁻ (x_1 : β), ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a ≠ ∞
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal)
    ((ν : (a : α) → Measure β) a)

Tactic:
refine integrable_toReal_of_lintegral_ne_top ?_ ?_

Premises used: MeasureTheory.integrable_toReal_of_lintegral_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)) ((ν : (a : α) → Measure β) a)

Tactic:
(Measurable.ennreal_ofReal ?_).aemeasurable

Premises used: Measurable.ennreal_ofReal, Measurable.aemeasurable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
refine_1 : Measurable (β := ℝ) fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)) ((ν : (a : α) → Measure β) a)

Tactic:
refine (Measurable.ennreal_ofReal ?_).aemeasurable

Premises used: Measurable.ennreal_ofReal, Measurable.aemeasurable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ Measurable (β := ℝ) fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x

Tactic:
(measurable_stieltjesOfMeasurableRat hf.measurable x).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.measurable_stieltjesOfMeasurableRat, ProbabilityTheory.IsRatCondKernelCDF.measurable, 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ Measurable (β := ℝ) fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x

Tactic:
exact (measurable_stieltjesOfMeasurableRat hf.measurable x).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.measurable_stieltjesOfMeasurableRat, ProbabilityTheory.IsRatCondKernelCDF.measurable, 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
refine_2 :
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (Iic x)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : β), ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a ≠ ∞

Tactic:
rw [lintegral_stieltjesOfMeasurableRat hf]

Premises used: ProbabilityTheory.lintegral_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (Iic x)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (α := Set β) univ (Iic x)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
hp :
  LE.le (α := ℝ) 0
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
hq : 0 ≤ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)

Tactic:
rw [← ENNReal.ofReal_eq_ofReal_iff, ofReal_measureReal]

Premises used: MeasureTheory.ofReal_measureReal, ENNReal.ofReal_eq_ofReal_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)

Tactic:
setIntegral_nonneg hs (fun _ _ ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_nonneg, Prod.mk, MeasureTheory.setIntegral_nonneg, ProbabilityTheory.IsRatCondKernelCDF.measurable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)

Tactic:
exact setIntegral_nonneg hs (fun _ _ ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_nonneg, MeasureTheory.setIntegral_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)

Tactic:
ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ 0 ≤ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)

Tactic:
exact ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hfi :
  @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)
f_nn :
  (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
    (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x
⊢ ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal, setLIntegral_stieltjesOfMeasurableRat hf _ _ hs]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
(integrable_stieltjesOfMeasurableRat hf _ _).restrict

Premises used: MeasureTheory.Integrable.restrict, ProbabilityTheory.integrable_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)

Tactic:
exact (integrable_stieltjesOfMeasurableRat hf _ _).restrict

Premises used: MeasureTheory.Integrable.restrict, ProbabilityTheory.integrable_stieltjesOfMeasurableRat
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
    (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x

Tactic:
ae_of_all _ (fun _ ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_nonneg, Prod.mk, MeasureTheory.ae_of_all, ProbabilityTheory.IsRatCondKernelCDF.measurable, Filter.EventuallyLE
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
    (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x

Tactic:
exact ae_of_all _ (fun _ ↦ stieltjesOfMeasurableRat_nonneg _ _ _)

Premises used: ProbabilityTheory.stieltjesOfMeasurableRat_nonneg, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
rw :
  (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) univ) fun (x_1 : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))
rw₁ rw₂ :
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))
⊢ (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))

Tactic:
rw [← setIntegral_univ, setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

Premises used: ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, MeasureTheory.setIntegral_univ, MeasurableSet.univ
-- 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 κ ν
a : α
q : ℚ
h : Measurable f := ⋯
⊢ ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α × β) ↦ f x a

Tactic:
rw [measurable_pi_iff] at h

Premises used: measurable_pi_iff
-- 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 κ ν
a : α
q : ℚ
h : ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α × β) ↦ f x a
⊢ Measurable (β := ℝ) fun (t : β) ↦ f (a, t) q

Tactic:
(h q).comp measurable_prodMk_left

Premises used: Measurable.comp, 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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α × β) ↦ f x a
⊢ Measurable (β := ℝ) fun (t : β) ↦ f (a, t) q

Tactic:
exact (h q).comp measurable_prodMk_left

Premises used: Measurable.comp, 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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
simp_rw :
  ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), f (a, a_1) i ≤ f (a, a_1) i_1
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → f (a, c) a_1 ≤ f (a, c) b

Tactic:
simp_rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- 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 κ ν
a : α
⊢ ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), f (a, a_1) i ≤ f (a, a_1) i_1

Tactic:
fun _ _ hqr ↦ hf.mono' a hqr

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), f (a, a_1) i ≤ f (a, a_1) i_1

Tactic:
exact fun _ _ hqr ↦ hf.mono' a hqr

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (q : ℚ), 0 ≤ f (a, c) q

Tactic:
ae_all_iff.mpr <| hf.nonneg' a

Premises used: Iff.mpr, ProbabilityTheory.IsRatCondKernelCDFAux.nonneg', MeasureTheory.ae_all_iff
-- 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 κ ν
a : α
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (q : ℚ), f (a, c) q ≤ 1

Tactic:
ae_all_iff.mpr <| hf.le_one' a

Premises used: Iff.mpr, ProbabilityTheory.IsRatCondKernelCDFAux.le_one', MeasureTheory.ae_all_iff
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 0)

Tactic:
tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_of_integral_tendsto_of_antitone, MeasureTheory.integrable_const
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
refine_2 :
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 0))
refine_3 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
refine_4 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 0)

Tactic:
refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_of_integral_tendsto_of_antitone, MeasureTheory.integrable_const
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)

Tactic:
fun n ↦ hf.integrable a (seq n)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable
-- 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 ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)

Tactic:
exact fun n ↦ hf.integrable a (seq n)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable