-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
/-- If a monotone sequence of functions has an upper bound and the sequence of integrals of these
functions tends to the integral of the upper bound, then the sequence of functions converges
almost everywhere to the upper bound. Auxiliary version assuming moreover that the
functions in the sequence are ae measurable. -/
lemma tendsto_of_lintegral_tendsto_of_monotone_aux {α : Type*} {mα : MeasurableSpace α}
    {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞} {μ : Measure α}
    (hf_meas : ∀ n, AEMeasurable (f n) μ) (hF_meas : AEMeasurable F μ)
    (hf_tendsto : Tendsto (fun i ↦ ∫⁻ a, f i a ∂μ) atTop (𝓝 (∫⁻ a, F a ∂μ)))
    (hf_mono : ∀ᵐ a ∂μ, Monotone (fun i ↦ f i a))
    (h_bound : ∀ᵐ a ∂μ, ∀ i, f i a ≤ F a) (h_int_finite : ∫⁻ a, F a ∂μ ≠ ∞) :
    ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Proof state:
case h
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a => if h : ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l) then h.choose else ⊤
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F' a))
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_tendsto : Tendsto (fun i => f i a) atTop (𝓝 (F' a))
⊢ F' a ≤ F a

Tactic:
exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)

Result:
no goals

Proof state:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))

Tactic:
have h_bound_finite : ∀ᵐ a ∂μ, F a ≠ ∞ := by
  filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne

Result:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))

Proof state:
case h.inl.intro
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_fin : F a ≠ ⊤
h_mono : Monotone fun i => f i a
h_absurd : ∀ (b : ℝ≥0∞), ∃ a_1, b ≤ f a_1 a
i : ℕ
hi : F a + 1 ≤ f i a
⊢ F a < F a + 1

Tactic:
exact ENNReal.lt_add_right h_fin one_ne_zero

Result:
no goals

Proof state:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a => if h : ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l) then h.choose else ⊤
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F' a))
hF'_le : F' ≤ᶠ[ae μ] F
⊢ F' =ᶠ[ae μ] F

Tactic:
suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
  ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le

Result:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a => if h : ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l) then h.choose else ⊤
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F' a))
hF'_le : F' ≤ᶠ[ae μ] F
⊢ ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ

Proof state:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, F a ≠ ⊤

Tactic:
filter_upwards [ae_lt_top' hF_meas h_int_finite] with a ha using ha.ne

Result:
no goals

Proof state:
α : Type u_5
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i => ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i => f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ⊤
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ⊤
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i => f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i => f i a) atTop (𝓝 (F a))

Tactic:
classical
let F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
  then h.choose else ∞
have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
  filter_upwards [h_exists] with a ha
  simp_rw [F', dif_pos ha]
  exact ha.choose_spec
suffices F' =ᵐ[μ] F by
  filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
have hF'_le : F' ≤ᵐ[μ] F := by
  filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
  exact le_of_tendsto' h_tendsto (fun m ↦ h_le _)
suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
  ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le
refine tendsto_nhds_unique ?_ hf_tendsto
exact lintegral_tendsto_of_tendsto_of_monotone hf_meas hf_mono hF'_tendsto

Result:
no goals