-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.tendsto_stieltjesFunction_atTop (a : α) :
    Tendsto (hf.stieltjesFunction a) atTop (𝓝 1)

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y ≤ ↑(qs y) + 1
⊢ q ≤ qs y

Tactic:
exact_mod_cast le_of_add_le_add_right (hy.trans h_le)

Result:
no goals

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ (f a ∘ qs) x ≤ ↑(hf.stieltjesFunction a) x

Tactic:
rw [Function.comp_apply, ← stieltjesFunction_eq hf]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ ↑(hf.stieltjesFunction a) ↑(qs x) ≤ ↑(hf.stieltjesFunction a) x

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le ((hf.tendsto_atTop_one a).comp hqs_tendsto)
    tendsto_const_nhds ?_ (stieltjesFunction_le_one hf a)

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
⊢ f a ∘ qs ≤ ↑(hf.stieltjesFunction a)

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
⊢ Tendsto qs atTop atTop

Tactic:
rw [tendsto_atTop_atTop]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
⊢ ∀ (b : ℚ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ qs a

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Tactic:
let qs : ℝ → ℚ := fun x ↦ (h_exists x).choose

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Tactic:
have hqs_tendsto : Tendsto qs atTop atTop := by
  rw [tendsto_atTop_atTop]
  refine fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩
  have h_le : y - 1 ≤ qs y := (h_exists y).choose_spec.1.le
  rw [sub_le_iff_le_add] at h_le
  exact_mod_cast le_of_add_le_add_right (hy.trans h_le)

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y - 1 ≤ ↑(qs y)
⊢ q ≤ qs y

Tactic:
rw [sub_le_iff_le_add] at h_le

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y ≤ ↑(qs y) + 1
⊢ q ≤ qs y

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
⊢ f a ∘ qs ≤ ↑(hf.stieltjesFunction a)

Tactic:
intro x

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ (f a ∘ qs) x ≤ ↑(hf.stieltjesFunction a) x

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Tactic:
have h_exists : ∀ x : ℝ, ∃ q : ℚ, x - 1 < q ∧ ↑q < x := fun x ↦ exists_rat_btwn (sub_one_lt x)

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
⊢ Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
⊢ ∀ (b : ℚ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ qs a

Tactic:
refine fun q ↦ ⟨q + 1, fun y hy ↦ ?_⟩

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
⊢ q ≤ qs y

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
⊢ q ≤ qs y

Tactic:
have h_le : y - 1 ≤ qs y := (h_exists y).choose_spec.1.le

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
q : ℚ
y : ℝ
hy : ↑q + 1 ≤ y
h_le : y - 1 ≤ ↑(qs y)
⊢ q ≤ qs y

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x
qs : ℝ → ℚ := fun x => ⋯.choose
hqs_tendsto : Tendsto qs atTop atTop
x : ℝ
⊢ ↑(hf.stieltjesFunction a) ↑(qs x) ≤ ↑(hf.stieltjesFunction a) x

Tactic:
exact (hf.stieltjesFunction a).mono (le_of_lt (h_exists x).choose_spec.2)

Result:
no goals