awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
this :
  ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst
⊢ ∫⁻ (x : α) in s, 1 x ∂ρ.fst.withDensity (preCDF ρ r) = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s

Tactic:
simp only [withDensity_preCDF ρ r, Pi.one_apply, lintegral_one, Measure.restrict_apply,
      MeasurableSet.univ, univ_inter]

Premises used: Pi.one_apply, MeasureTheory.Measure.restrict_apply, Set.univ_inter, ProbabilityTheory.withDensity_preCDF, MeasurableSet.univ, MeasureTheory.lintegral_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
this :
  ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ 1

Tactic:
measurable_const

Premises used: measurable_const
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
this :
  ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ 1

Tactic:
exact measurable_const

Premises used: measurable_const
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst : IsFiniteMeasure ρ
rw : ∫⁻ (x : α) in univ, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ∫⁻ (x : α), preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ

Tactic:
rw [← setLIntegral_univ, setLIntegral_preCDF_fst ρ r MeasurableSet.univ]

Premises used: ProbabilityTheory.setLIntegral_preCDF_fst, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
simp_rw : ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a
⊢ ∀ᵐ (a : α) ∂ρ.fst, Monotone (β := ℝ≥0∞) fun (r : ℚ) ↦ preCDF ρ r a

Tactic:
simp_rw [Monotone, ae_all_iff]

Premises used: Monotone, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a

Tactic:
fun r r' hrr' ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF
    fun s hs _ ↦ ?_

Premises used: ProbabilityTheory.measurable_preCDF, Filter.EventuallyLE, MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
refine :
  ∀ (r r' : ℚ) (hrr' : r ≤ r') (s : Set α) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, preCDF ρ r' x ∂ρ.fst
⊢ ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a

Tactic:
refine fun r r' hrr' ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF
    fun s hs _ ↦ ?_

Premises used: ProbabilityTheory.measurable_preCDF, MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ.IicSnd (↑r' : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, preCDF ρ r' x ∂ρ.fst

Tactic:
rw [setLIntegral_preCDF_fst ρ r hs, setLIntegral_preCDF_fst ρ r' hs]

Premises used: ProbabilityTheory.setLIntegral_preCDF_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ.IicSnd (↑r' : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
Measure.IicSnd_mono ρ (mod_cast hrr') s

Premises used: MeasureTheory.Measure.IicSnd_mono
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ρ.IicSnd (↑r' : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact Measure.IicSnd_mono ρ (mod_cast hrr') s

Premises used: MeasureTheory.Measure.IicSnd_mono
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
rw : ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1
⊢ ∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ℚ), preCDF ρ r a ≤ 1

Tactic:
rw [ae_all_iff]

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1

Tactic:
fun r ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF fun s hs _ ↦ ?_

Premises used: ProbabilityTheory.measurable_preCDF, Filter.EventuallyLE, MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
refine :
  ∀ (r : ℚ) (s : Set α) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
⊢ ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1

Tactic:
refine fun r ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF fun s hs _ ↦ ?_

Premises used: ProbabilityTheory.measurable_preCDF, MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst

Tactic:
rw [setLIntegral_preCDF_fst ρ r hs]

Premises used: ProbabilityTheory.setLIntegral_preCDF_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
simp : LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst

Tactic:
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ, MeasureTheory.lintegral_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
Measure.IicSnd_le_fst ρ r s

Premises used: Rat.cast, MeasureTheory.Measure.IicSnd_le_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact Measure.IicSnd_le_fst ρ r s

Premises used: Rat.cast, MeasureTheory.Measure.IicSnd_le_fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
rw : (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd (↑r : ℝ)).real s
hfm : AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)
hf : ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ∞
⊢ ∫ (x : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real s

Tactic:
rw [integral_toReal]

Premises used: MeasureTheory.integral_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
rw : ENNReal.toReal ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s) = (ρ.IicSnd (↑r : ℝ)).real s
rw₁ rw₂ :
  ENNReal.toReal ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s) =
    ENNReal.toReal ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s)
⊢ (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd (↑r : ℝ)).real s

Tactic:
rw [setLIntegral_preCDF_fst _ _ hs, measureReal_def]

Premises used: ProbabilityTheory.setLIntegral_preCDF_fst, MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)

Tactic:
measurable_preCDF.aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.measurable_preCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)

Tactic:
exact measurable_preCDF.aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.measurable_preCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ∞

Tactic:
ae_restrict_of_ae ?_

Premises used: MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
hf : ∀ᵐ (x : α) ∂ρ.fst, preCDF ρ r x < ∞
⊢ ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ∞

Tactic:
refine ae_restrict_of_ae ?_

Premises used: MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
h : ∀ (a : α) (ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1), preCDF ρ r a < ∞
⊢ ∀ᵐ (x : α) ∂ρ.fst, preCDF ρ r x < ∞

Tactic:
filter_upwards [preCDF_le_one ρ] with a ha

Premises used: ProbabilityTheory.preCDF_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a < ∞

Tactic:
(ha r).trans_lt ENNReal.one_lt_top

Premises used: ENNReal.one_lt_top, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ r a < ∞

Tactic:
exact (ha r).trans_lt ENNReal.one_lt_top

Premises used: ENNReal.one_lt_top, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst : IsFiniteMeasure ρ
rw : ∫ (x : α) in univ, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real univ
rw₁ rw₂ : (ρ.IicSnd (↑r : ℝ)).real univ = (ρ.IicSnd (↑r : ℝ)).real univ
⊢ ∫ (x : α), (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real univ

Tactic:
rw [← setIntegral_univ, setIntegral_preCDF_fst ρ _ MeasurableSet.univ]

Premises used: ProbabilityTheory.setIntegral_preCDF_fst, MeasureTheory.setIntegral_univ, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst

Tactic:
integrable_of_forall_fin_meas_le _ (measure_lt_top ρ.fst univ) ?_ fun t _ _ ↦ ?_

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.integrable_of_forall_fin_meas_le, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst
refine_2 :
  ∀ (t : Set α),
    MeasurableSet t →
      Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x_3 : α) in t, ‖(preCDF ρ x x_3).toReal‖ₑ ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst

Tactic:
refine integrable_of_forall_fin_meas_le _ (measure_lt_top ρ.fst univ) ?_ fun t _ _ ↦ ?_

Premises used: MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.integrable_of_forall_fin_meas_le, MeasureTheory.Measure.fst
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst

Tactic:
measurable_preCDF.ennreal_toReal.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, ProbabilityTheory.measurable_preCDF, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst

Tactic:
exact measurable_preCDF.ennreal_toReal.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, ProbabilityTheory.measurable_preCDF, Measurable.ennreal_toReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ
⊢ ∫⁻ (x_1 : α) in t, ‖(preCDF ρ x x_1).toReal‖ₑ ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ

Tactic:
simp_rw [← ofReal_norm, Real.norm_of_nonneg ENNReal.toReal_nonneg]

Premises used: ENNReal.toReal_nonneg, ofReal_norm, Real.norm_of_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ

Tactic:
rw [← lintegral_one]

Premises used: MeasureTheory.lintegral_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst

Tactic:
(setLIntegral_le_lintegral _ _).trans (lintegral_mono_ae ?_)

Premises used: MeasureTheory.lintegral_mono_ae, LE.le.trans, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst

Tactic:
refine (setLIntegral_le_lintegral _ _).trans (lintegral_mono_ae ?_)

Premises used: MeasureTheory.lintegral_mono_ae, LE.le.trans, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1

Tactic:
ENNReal.ofReal_toReal_le.trans (ha _)

Premises used: ENNReal.ofReal_toReal_le, LE.le.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h_1 : MeasurableSet t
h_2 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (r : ℚ), preCDF ρ r a ≤ 1) x} x_1 →
          Membership.mem (γ := Set α) {x_2 : α | (fun (a : α) ↦ ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1) x_2} x_1}
      a
h₁ h₂ : ∀ (a : α) (ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1), ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1
⊢ ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1

Tactic:
filter_upwards [preCDF_le_one ρ] with a ha using ENNReal.ofReal_toReal_le.trans (ha _)

Premises used: ProbabilityTheory.preCDF_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
r r' : ℚ
hrr' : r ≤ r'
h :
  ∀ (a : α) (h₁ : Monotone (β := ℝ≥0∞) fun (r : ℚ) ↦ preCDF ρ r a) (h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1),
    (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal
⊢ ∀ᵐ (c : α) ∂((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a : Measure α),
    (preCDF ρ r (a, c).2).toReal ≤ (preCDF ρ r' (a, c).2).toReal

Tactic:
filter_upwards [monotone_preCDF ρ, preCDF_le_one ρ] with a h₁ h₂

Premises used: ProbabilityTheory.preCDF_le_one, ProbabilityTheory.monotone_preCDF
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a_1 : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone (β := ℝ≥0∞) fun (r : ℚ) ↦ preCDF ρ r a
h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal

Tactic:
ENNReal.toReal_mono ((h₂ _).trans_lt ENNReal.one_lt_top).ne (h₁ hrr')

Premises used: ENNReal.one_lt_top, LE.le.trans_lt, ENNReal.toReal_mono, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a_1 : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone (β := ℝ≥0∞) fun (r : ℚ) ↦ preCDF ρ r a
h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal

Tactic:
exact ENNReal.toReal_mono ((h₂ _).trans_lt ENNReal.one_lt_top).ne (h₁ hrr')

Premises used: ENNReal.one_lt_top, LE.le.trans_lt, ENNReal.toReal_mono, LT.lt.ne
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) x : Measure α), 0 ≤ (preCDF ρ q (x, c).2).toReal

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
q : ℚ
simp : ∀ᵐ (c : α) ∂ρ.fst, (preCDF ρ q c).toReal ≤ 1
⊢ ∀ᵐ (c : α) ∂((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a : Measure α), (preCDF ρ q (a, c).2).toReal ≤ 1

Tactic:
simp only [Kernel.const_apply]

Premises used: ProbabilityTheory.Kernel.const_apply
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
q : ℚ
h : ∀ (a : α) (ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1), (preCDF ρ q a).toReal ≤ 1
⊢ ∀ᵐ (c : α) ∂ρ.fst, (preCDF ρ q c).toReal ≤ 1

Tactic:
filter_upwards [preCDF_le_one ρ] with a ha

Premises used: ProbabilityTheory.preCDF_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a_1 : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ q a).toReal ≤ 1

Tactic:
ENNReal.toReal_le_of_le_ofReal zero_le_one ?_

Premises used: zero_le_one, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a_1 : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
h : preCDF ρ q a ≤ ENNReal.ofReal 1
⊢ (preCDF ρ q a).toReal ≤ 1

Tactic:
refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_

Premises used: zero_le_one, ENNReal.toReal_le_of_le_ofReal
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a_1 : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ q a ≤ ENNReal.ofReal 1

Tactic:
simp [ha]
-- Module: Mathlib.Probability.Kernel.Disintegration.CondCDF
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h : Antitone s
hs_tendsto : Tendsto s atTop atBot
simp_rw : Tendsto (β := ℝ) (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mα ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) fun (c : α) ↦
        (preCDF ρ (s m) (a, c).2).toReal)
    atTop (𝓝 0)

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 : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ) atBot (𝓝 0)

Tactic:
have h := ρ.tendsto_IicSnd_atBot MeasurableSet.univ
-- 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)
⊢ Tendsto ENNReal.toReal (𝓝 0) (𝓝 0)

Tactic:
have h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0) :=
      ENNReal.continuousAt_toReal ENNReal.zero_ne_top
-- 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:
h0.comp (h.comp hs_tendsto)

Premises used: MeasureTheory.Measure.real, ENNReal.toReal, Filter.Tendsto.comp, NNReal.toReal