-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma isRatCondKernelCDFAux_preCDF (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] :
    IsRatCondKernelCDFAux (fun p r ↦ (preCDF ρ r p.2).toReal)
      (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst) where
  measurable := measurable_preCDF'.comp measurable_snd
  mono' a r r' hrr'

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 0)

Tactic:
have h := ρ.tendsto_IicSnd_atBot MeasurableSet.univ

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 0)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ENNReal.toReal 0))

Tactic:
have h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0) :=
  ENNReal.continuousAt_toReal ENNReal.zero_ne_top

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)
h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ENNReal.toReal 0))

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atTop (𝓝 (ρ.fst univ))
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)

Tactic:
have h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst univ).toReal) :=
  ENNReal.continuousAt_toReal (measure_ne_top _ _)

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atTop (𝓝 (ρ.fst univ))
h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst univ).toReal)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m => ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop
    (𝓝 (((Kernel.const Unit ρ.fst) a) univ).toReal)

Tactic:
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atTop (𝓝 (ρ.fst univ))
h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst univ).toReal)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)

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

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m => ∫ (c : α), (preCDF ρ (s m) (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a) atTop (𝓝 0)

Tactic:
simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 0)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ q a ≤ ENNReal.ofReal 1

Tactic:
simp [ha]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 0)

Tactic:
rw [← ENNReal.zero_toReal]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atBot (𝓝 0)
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ENNReal.toReal 0))

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂ρ.fst, (preCDF ρ q c).toReal ≤ 1

Tactic:
filter_upwards [preCDF_le_one ρ] with a ha

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ q a).toReal ≤ 1

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂(Kernel.const Unit ρ.fst) a =
    (((Kernel.const Unit ρ) a) (s ×ˢ Iic ↑q)).toReal

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

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone 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')

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x✝ : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) x✝, 0 ≤ (preCDF ρ q (x✝, c).2).toReal

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
r r' : ℚ
hrr' : r ≤ r'
⊢ ∀ᵐ (c : α) ∂(Kernel.const Unit ρ.fst) a, (preCDF ρ r (a, c).2).toReal ≤ (preCDF ρ r' (a, c).2).toReal

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

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
r r' : ℚ
hrr' : r ≤ r'
a : α
h₁ : Monotone fun r => preCDF ρ r a
h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)

Tactic:
have h := ρ.tendsto_IicSnd_atTop MeasurableSet.univ

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
h : Tendsto (fun r => (ρ.IicSnd ↑r) univ) atTop (𝓝 (ρ.fst univ))
⊢ Tendsto (fun m => ((ρ.IicSnd ↑(s m)) univ).toReal) atTop (𝓝 (ρ.fst univ).toReal)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ q a).toReal ≤ 1

Tactic:
refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a✝ : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ preCDF ρ q a ≤ ENNReal.ofReal 1