Supremum of largest interval where f is positive

Stream: new members

[Mario F.]

I want to show that a continuous function f : ℝ → ℝ is positive for all t > 0. On paper, I would consider the largest interval (0, t₀) where this is the case, i.e., S := {t > 0 | ∀ t₁ ∈ (Ioo 0 t), f t₁ > 0}. If f 0 > 0, the set is nonempty by continuity. Assuming its supremum t₀ is finite, we have ∀ t₁ ∈ (Ioo 0 t₀), f t₁ > 0 and f t₀ = 0 by definition of the supremum and continuity. Using further properties of f, I can then derive at a contradiction. (This basically means that I have a look at the smallest counterexample.)

I have no idea how to translate this to Lean. Mainly, I do not understand how to work with suprema of real sets at all. Next, I believe I should use filters whenever possible. For instance,

example {f : ℝ → ℝ} (f_null_pos : f 0 > 0) (f_cont_0 : ContinuousAt f 0):
  ∀ᶠ t in (𝓝 0), 0 < f t
  := Filter.Tendsto.eventually_const_lt f_null_pos (f_cont_0.tendsto)

is quickly proven. On the other hand, while I can also prove ∃ t₂ > 0, ∀ t ∈ (Ioo 0 t₂), f t > 0, my proof uses some lengthy epsilon-delta rewrites, I would rather avoid. Moreover, for the contradiction that the end, I would like to make use of something like ∀ᶠ t in (𝓝[<] t₀), f t > 0, so also there filters are to be preferred.

This leaves me to believe that a proof by such a set S is not the canonical way to do this in Lean. How else can I approach this?

[Kenny Lau]

what if you take instead the infimum of { t > 0 | f t <= 0 }?

[Kenny Lau]

import Mathlib

example (f : ℝ → ℝ) (h₁ : ∀ t₀ : ℝ, 0 < t₀ → (∀ x ∈ Set.Ioo 0 t₀, 0 < f x) → f t₀ ≤ 0 → False)
    (t : ℝ) : 0 < f t := by
  refine lt_of_not_ge fun hft ↦ h₁ (sInf { s | 0 < s ∧ f s ≤ 0 }) ?_
    (fun x hx ↦ lt_of_not_ge fun hfx ↦ not_le_of_gt hx.2 ?_) ?_
  · sorry -- this uses continuity
  · sorry -- uh... is this a missing lemma?
  · sorry -- this uses continuity too

[Kenny Lau]

this is basically what i'm proposing, there might be some missing lemmas as well

[Kenny Lau]

maybe other people can give you more helpful pointers than i can

[Aaron Liu]

import Mathlib

theorem Metric.frequently_nhds_iff {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} :
    (∃ᶠ (y : α) in nhds x, p y) ↔ ∀ ε > 0, ∃ y : α, dist y x < ε ∧ p y := by
  rw [← not_iff_not, Filter.not_frequently, Metric.eventually_nhds_iff]
  simp

example {f : ℝ → ℝ} (hf : Continuous f) (h₁ : ∀ t₀ : ℝ, 0 < t₀ → (∀ x ∈ Set.Ioo 0 t₀, 0 < f x) → f t₀ ≤ 0 → False)
    (h₂ : 0 < f 0) ⦃t : ℝ⦄ (ht : 0 < t) : 0 < f t := by
  replace h₁ (t₀ : ℝ) (ht₀ : 0 ≤ t₀) (hoo : ∀ x ∈ Set.Ioo 0 t₀, 0 < f x) (hft : f t₀ ≤ 0) : False := by
    obtain htp | rfl := lt_or_eq_of_le ht₀
    · exact h₁ t₀ htp hoo hft
    · exact h₂.not_ge hft
  refine lt_of_not_ge fun hft ↦ h₁ (sInf { s | 0 < s ∧ f s ≤ 0 }) ?_
    (fun x hx ↦ lt_of_not_ge fun hfx ↦ not_le_of_gt hx.2 ?_) ?_
  · exact (le_csInf ⟨t, ht, hft⟩ fun c hc => hc.left.le)
  · apply csInf_le
    · use 0
      intro c hc
      exact hc.left.le
    · exact ⟨hx.left, hfx⟩
  · rw [← Set.mem_Iic]
    refine Filter.Frequently.mem_of_closed ?_ isClosed_Iic
    refine Filter.Frequently.filter_mono ?_ (hf.tendsto _)
    rw [Filter.frequently_map, Metric.frequently_nhds_iff]
    intro ε hε
    have hi : {s | 0 < s ∧ f s ≤ 0}.Nonempty := ⟨t, ht, hft⟩
    obtain ⟨y, hy, hyε⟩ := Real.lt_sInf_add_pos hi hε
    refine ⟨y, ?_, hy.right⟩
    rw [Real.dist_eq, abs_lt, neg_lt_sub_iff_lt_add, sub_lt_iff_lt_add']
    refine ⟨?_, hyε⟩
    apply lt_add_of_pos_of_le hε
    refine csInf_le ?_ hy
    use 0
    intro c hc
    exact hc.left.le

[Mario F.]

Thanks! I learned a lot while checking your proofs, not only how to actually use supremum/infimum but also some nice Lean tricks (or perhaps some Lean basics?).

The code by Aaron Liu works, but I wonder whether the epsilon proof at the end is necessary? There exists a sequence of numbers in the set (on each fof which f is nonpositive) converging to the infimum. By continuity, f is also nonpositive at the infimum. There surely is a filter version of this proof which works well with what Lean already knows about infima?