Why does this theorem leads to contradiction?

Stream: new members

[Arshak Parsa]

import Mathlib
open MeasureTheory Filter Set ProbabilityTheory Topology

lemma F_tendsto_atBot_inf {f : ℝ → ℝ} (hf : Integrable f) :
    Tendsto (fun x ↦ ∫ (t : ℝ) in Iic x, f t) atBot (𝓝 0) := by
  let s := fun i : ℝ => Iic (i)
  have hmono : Monotone (⇑volume ∘ s) := by
    unfold_let
    rw [monotone_iff_forall_lt]
    aesop
  have h1 : Tendsto (⇑ℙ ∘ s) atBot (𝓝 (⨅ i, (⇑ℙ ∘ s) i)) := by
    exact tendsto_atBot_iInf hmono
  have hiInf : (⨅ i, (⇑ℙ ∘ s) i) = 0 := by
    unfold_let
    simp only [Function.comp_apply]
    simp only [Real.volume_Iic]
    rw [iInf]
    simp
    sorry
  rw [hiInf] at h1
  exact Integrable.tendsto_setIntegral_nhds_zero hf h1

After simp my goal becomes False.
btw could someone prove this theorem, it is too hard for me :/

[Arshak Parsa]

Is there a better notation for limit ?
like lim x → -∞ , (∫ (t : ℝ) in Iic x, f t) = 0 instead of Tendsto (fun x ↦ ∫ (t : ℝ) in Iic x, f t) atBot (𝓝 0)

[Eric Wieser]

hiInf is false before the second simp only because the goal is ⨅ i, ℙ (Iic i) = 0, but in fact ⨅ i, ℙ (Iic i) = ∞

[Eric Wieser]

What's the math proof?

[Arshak Parsa]

Is f(x) = x integrable ?
It is true only for integrable integrals.
(Actually, I am trying to prove that the limit of cumulative distribution function is 0 at -inf :grimacing:)

[Arshak Parsa]

Well, I guess it doesn't need a proof because when Iic x goes to negative infinity, it is approaching the empty set, and the integral of empty set is zero.
(I am assuming that my integral is finite and positive)

[Arshak Parsa]

You are right, I think I need to add the f x > 0 to my hypothesis

[Arshak Parsa]

lemma F_tendsto_atBot_inf {f : ℝ → ℝ} (hf : Integrable f) (hpos : ∀x, f x ≥ 0):
    Tendsto (fun x ↦ ∫ (t : ℝ) in Iic x, f t) atBot (𝓝 0) := by
  sorry

this is my lemma

[Etienne Marion]

Hi! Here is a proof using dominated convergence theorem, you don't need nonnegativity assumption.

import Mathlib

open MeasureTheory Filter Set ProbabilityTheory Topology

lemma F_tendsto_atBot_inf {f : ℝ → ℝ} (hf : Integrable f) :
    Tendsto (fun x ↦ ∫ (t : ℝ) in Iic x, f t) atBot (𝓝 0) := by
  have this (x : ℝ) : ∫ t in Iic x, f t = ∫ t, (Iic x).indicator f t :=
    (integral_indicator measurableSet_Iic).symm
  simp_rw [this]
  rw [← integral_zero]
  apply tendsto_integral_filter_of_dominated_convergence (fun x ↦ ‖f x‖)
  · exact eventually_of_forall fun x ↦ hf.aestronglyMeasurable.indicator measurableSet_Iic
  · exact eventually_of_forall fun x ↦ eventually_of_forall fun y ↦ norm_indicator_le_norm_self _ _
  · exact hf.norm
  · refine eventually_of_forall fun x ↦ tendsto_const_nhds.congr' ?_
    rw [EventuallyEq, eventually_atBot]
    refine ⟨x - 1, fun y hy ↦ ?_⟩
    simp [Set.indicator, (by linarith : ¬x ≤ y)]

[Notification Bot]

Arshak Parsa has marked this topic as resolved.

[Notification Bot]

Eric Wieser has marked this topic as unresolved.

[Eric Wieser]

I wonder if mathlib should have this result, and similarly for atTop?

[Eric Wieser]

Maybe an analyst can chime in (unresolving for visibility)

[Arshak Parsa]

Nice!

[Arshak Parsa]

I also need another theorem :grimacing:

[Etienne Marion]

Feel free to ask if you have any trouble!

[Sébastien Gouëzel]

Note that it should be possible to remove also the integrability assumption, as non-integrable functions have zero integral.