Proofs about garbage values?

Stream: new members

[Adomas Baliuka]

Functions such as log or division are defined in Mathlib on all of the reals and "garbage values" (often zero) are used where the common mathematical definition would not define such functions at all. This leads to a lot of "theorems" which aren't true in mathematics. How does one deal with that?

One way is to accept that Real.log isn't the same as the logarithm function used in mathematics, log 0 = 0 / 0 = 0 really holds and make all theorems as general as possible. Another way is to "pretend" that these functions are the same as in math and try to "never divide by zero". I think the second way is very hard to maintain (tactics would need to know this? Does that then defeat the purpose of formally verifying stuff?) and there are a lot of theorems in mathlib already which use the definitions as they are (e.g. unnecessary differentiability assumptions are omitted).

On the other hand, there seem to be theorems in Mathlib that could be generalized but weren't, perhaps due to not being "true in math".

For example, I'm reasonably sure (my recent question on this didn't receive answers) that Continuous fun x => x * Real.log x. Is that something that could go into Mathlib if proven, or is it a "bad theorem"?

[Kevin Buzzard]

You say "I think the second way is very hard to maintain" but 10^6+ lines of mathlib code is evidence against that claim, right?

There are certainly theorems in mathlib like (a+b)/c=a/c+b/c which are true more generally in Lean than in real maths, and your continuity statement is another such example, so I don't see why it couldn't go in mathlib.

[Adomas Baliuka]

So which is the way this is dealt with? Is it "neither, there's more nuance than choosing one approach"?

You seem to be implying that there is something about this that needs to be maintained manually (presumably, that theorem statements don't stray too far from what's true in standard math) but my example would be OK despite not being true in normal math? I don't quite understand. Are there "evil theorems" that typecheck but aren't "true" in some sense relevant to Mathlib and would be bad to include (I'm not talking about "theorems that break tactics" or "trivial theorems that just clutter the code")? Is it true to say that a theorem that's already in Mathlib should always be as general as possible (have the weakest possible assumptions)?

[Ruben Van de Velde]

Have you read the Xena blog post about division by zero?

[Adomas Baliuka]

Ruben Van de Velde said:

Have you read the Xena blog post about division by zero?

Yes, the way I understand it it has the same tension between "mathematicians never divide by zero" (I would think this implies that my continuity statement is "bad") and "division as defined in Lean is not the same as in Math" (which I would think means my continuity statement is OK)

[Ruben Van de Velde]

Basically yes, I'd say you want to expect that lean definitions can be somewhat more general than you'd usually make them in mathematics. I'm not sure I'd talk about theorems that are false in mathematics: they're theorems whose statement is meaningless in most "informal" mathematics

[Riccardo Brasca]

If you really want you can prove "false" theorems, for example: there exist a rational x such that 1 / x = 2 / x.

[Riccardo Brasca]

I mean, theorems that a mathematician would say are false.

[Eric Rodriguez]

I think it's actually in the spirit of mathlib to prove statements that are generally true given the garbage value. Often the garbage value is chosen so that some good amount of theorems are true in this case (e.g. why do we have (2 : Nat) - 4 = 0 instead of 37?) and some of the beauty of this is creating really nice api that requires slightly less than usual, as it saves keystrokes, assumptions and pain. (The tsub API is a good example of this).

[Eric Rodriguez]

These sometimes orchestrate in a nice way for advanced maths, too; in flt-regular Riccardo has proved a nice formula for the discriminant of Q[zeta_p^n] that unifies all cases (even p^k = 1, 2) whilst the "usual" way the formula is presented is with cases. We've often found that the cardinality of infinite groups being set to zero can be really helpful due to divisibility orderings also having zero as the top element.

[Adomas Baliuka]

I proved

lemma continuous_log_mul_rpow {r : ℝ} (hr : 0 < r)
: Continuous (fun (x : ℝ) ↦ log x * x ^ r)

I'm sure this is about 10x longer and more ugly than what someone familiar with Lean/Mathlib would have written, but here it is:

/-
Copyright (c) 2023 Adomas Baliuka. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adomas Baliuka
-/
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

open Classical
open Filter
open Set
open Topology

/-!
# Assymptotics of `x^r * log x` near zero

In Mathlib, the Real natural logarithm is defined as `log |⬝|` (and zero at zero).
Real powers are defined such that
    · For `x > 0`, `x ^ y = exp (y log x)`.
    · For `x < 0`, `x ^ y = exp (y log x) cos (π y)`

Together, this implies that for `r > 0` the funciton `x ↦ x^r * log x` is continuous over ℝ.
For `x > 0`, this is proved in `tendsto_log_mul_rpow_nhds_zero`
(see `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics`)
This file generalizes to arbitrary `x : ℝ`.

The main result is `continuous_log_mul_rpow`.
Also provided are two generalizations of `tendsto_log_mul_rpow_nhds_zero`:
`tendsto_log_mul_rpow_nhds_zero'` (replaces `𝓝[>]` by `𝓝[≥]`)
`tendsto_log_mul_rpow_nhds_zero''` (replaces `ndhdsWithin` by `nhds`)
Probably only the second, most general should be kept? TODO

## Tags

limit, log, logarithm, xlogx, asymptotics, asymptotic, real, continuous, zero

-/

namespace AssymptoticsXPowlogX

section SetStuff  ------------------------------------------------------------------------

@[simp] lemma intersect_Ici_x_singleton {x : ℝ} : Ici (x : ℝ) ∩ {x} = {x} := by simp

lemma inters_subset_of_subset {s t U : Set α} (h : s ⊆ t)
    : U ∩ s ⊆ t := by
    intro x hx
    simp_all only [mem_inter_iff]
    apply h
    simp_all only

lemma Ioi_subset_iff_Iio_subset_neg {b : Set ℝ} : Ioi 0 ⊆ b ↔ Iio 0 ⊆ -b := by
    have subset_neg (A B : Set ℝ) : A ⊆ B ↔ -A ⊆ -B := Iff.symm neg_subset_neg
    convert subset_neg ?_ b
    simp

lemma Iio_zero_subset_iff_Ioi_subset_neg {b : Set ℝ}
: Iio 0 ⊆ b ↔ Ioi 0 ⊆ -b := by
    have subset_neg (A B : Set ℝ) : A ⊆ B ↔ -A ⊆ -B := Iff.symm neg_subset_neg
    convert subset_neg ?_ b
    simp

end SetStuff

section TendstoHelpers -------------------------------------------------------------------

lemma helper_tendsto_within_ge0 (f : ℝ → ℝ) (h: Tendsto f (𝓝[>] 0) (𝓝 0))
: Tendsto f (𝓝[Ici 0 ∩ {0}ᶜ] 0 ) (𝓝 0) := by
    have : Ici (0 : ℝ) ∩ {0}ᶜ = Ioi 0 := by
        ext x
        constructor
        rintro ⟨hl, hr⟩
        exact Ne.lt_of_le' hr hl
        intro
        simp_all
        constructor <;> linarith
    rw [this]
    exact h

lemma tendsto_of_union_tendstoWithin' {f : ℝ → ℝ} {l : Filter ℝ} {s1 s2 U : Set ℝ} {x : ℝ}
    (h_union : s1 ∪ s2 = U)
    (hl : Tendsto f (𝓝[s1] x) l)
    (hr : Tendsto f (𝓝[s2] x) l)
    : Tendsto f (𝓝[U] x) l := by
    let S := (s2 \ s1)
    have Ssubs2 : U ∩ S ⊆ s2 := by
        have := diff_subset s2 s1
        simp [S]
        exact inters_subset_of_subset this
    have Scomplsubs1 : U ∩ Sᶜ ⊆ s1 := by
        simp only [S] at *
        intro x hx
        rw [←h_union] at *
        simp_all only [compl_sdiff, mem_inter_iff, mem_union]
        have hx1 := hx.1
        have hx2 := hx.2
        cases hx1
        · simp_all only
        · apply hx2
          assumption
    have hl : Tendsto f (𝓝[U ∩ Sᶜ] x) l := by
        apply tendsto_nhdsWithin_mono_left Scomplsubs1 hl
    have hr : Tendsto f (𝓝[U ∩ S] x) l := by
        apply tendsto_nhdsWithin_mono_left Ssubs2 hr
    have := Tendsto.piecewise_nhdsWithin hr hl
    simp at this
    exact this

lemma tendsto_of_union_tendstoWithin {f : ℝ → ℝ} {l : Filter ℝ} {s1 s2 : Set ℝ} {x : ℝ}
    (h_union : s1 ∪ s2 = univ)
    (hl : Tendsto f (𝓝[s1] x) l)
    (hr : Tendsto f (𝓝[s2] x) l)
    : Tendsto f (𝓝 x) l := by
    convert tendsto_of_union_tendstoWithin' h_union hl hr
    exact (nhdsWithin_univ x).symm

lemma union_Ici_Iic_univ {x : ℝ} : Ici x ∪ Iic x = univ := by
    ext a
    simp only [mem_union, mem_Ici, mem_Iic, mem_univ, iff_true]
    exact le_total x a

lemma tendsto_ge_of_tendsto_gt_funvalue {f : ℝ → ℝ}
    (tenF : Tendsto f (𝓝[>] 0) (𝓝 0))
    (tenG : f 0 = 0)
: Tendsto f (𝓝[≥] 0) (𝓝 0) := by
    have h1 := helper_tendsto_within_ge0 f tenF
    have h2 : Tendsto f (𝓝[Ici 0 ∩ {0}] 0) (𝓝 0) := by
        simp
        exact EventuallyEq.tendsto tenG
    have := Tendsto.piecewise_nhdsWithin h2 h1
    simp at this
    exact this

lemma tendsto_zero_of_abs_tendsto_zero {f : ℝ → ℝ} {l : Filter ℝ}
    (tenF : Tendsto (fun x ↦ |f x|) l (𝓝 0))
    : Tendsto f l (𝓝 0) := by
    exact (tendsto_zero_iff_abs_tendsto_zero f).mpr tenF

lemma zero_le_abs_fun (f : ℝ → ℝ)  :
   0 ≤ fun x => |f x| := by
   intro x
   simp

lemma tendsto_zero_of_abs_le_tendsto_zero {g : ℝ → ℝ} {b : Filter ℝ}
    (f : ℝ → ℝ)
    (gLeF : |g| ≤ f)
    (tenF : Tendsto f b (𝓝 0))
    : Tendsto g b (𝓝 0) := by
    apply tendsto_zero_of_abs_tendsto_zero
    have hg : Tendsto (fun (_ : ℝ) ↦ (0 : ℝ)) b (𝓝 0) := tendsto_const_nhds
    refine tendsto_of_tendsto_of_tendsto_of_le_of_le hg tenF ?_ gLeF
    refine le_of_sub_nonneg ?tenF.hgf.a
    have : ((fun x => |g x|) - fun x => 0) = (fun x => |g x|) := by
        ext
        simp
    rw [this]
    exact zero_le_abs_fun fun x => g x

lemma preim_neg_nhdsWithin_zero {U : Set ℝ}
    : Neg.neg ⁻¹' U ∈ 𝓝[>] 0 ↔ U ∈ 𝓝[<] 0 := by
        simp_all
        constructor <;> intro h
        · simp [nhdsWithin] at *
          simp [Inf.inf] at *
          rcases h with ⟨a, ⟨ha, b, ⟨hb1, hb2⟩⟩⟩
          use -a
          constructor
          · exact neg_mem_nhds_zero ℝ ha
          · use -b
            constructor
            · exact (Ioi_subset_iff_Iio_subset_neg).mp hb1
            · exact neg_eq_iff_eq_neg.mp hb2
        · simp [nhdsWithin] at *
          simp [Inf.inf] at *
          rcases h with ⟨a, ⟨ha, b, ⟨hb1, hb2⟩⟩⟩
          use -a
          constructor
          · exact neg_mem_nhds_zero ℝ ha
          · use -b
            constructor
            · exact (Iio_zero_subset_iff_Ioi_subset_neg).mp hb1
            · simp_all only [inter_neg]

lemma tendsto_nhdsWithin_of_tendsto_nhdsWithin_neg
   {f : ℝ → ℝ}
   {l : Filter ℝ}
   : Tendsto f (𝓝[<] 0) l
   ↔ Tendsto (fun x ↦ f (-x)) (𝓝[>] 0) l := by
    have : (fun (x : ℝ) ↦ f (-x)) = f ∘ Neg.neg := by ext; simp
    rw [this]
    constructor <;> intro h
    · apply Tendsto.comp h
      convert tendsto_neg_nhdsWithin_Ioi
      simp; simp; exact TopologicalRing.toContinuousNeg
    · intro U hU
      simp only [Tendsto, LE.le] at h
      simp_all
      have := h hU
      have preim_comp : f ∘ Neg.neg ⁻¹' U = Neg.neg ⁻¹' (f ⁻¹' U) := by rfl
      rw [preim_comp] at this
      exact preim_neg_nhdsWithin_zero.mp this

lemma zero_mem_iff_zero_mem_neg (U : Set ℝ)
    : 0 ∈ U ↔ 0 ∈ -U := by
    simp_all only [Set.mem_neg, neg_zero]

end TendstoHelpers

section XLogX --------------------------------------------------------------------------

open Real

lemma tendsto_rpow_neg {r : ℝ} (hr : 0 < r)
 : Tendsto (fun x => log x * (-x) ^ r) (𝓝[>] 0) (𝓝 0) := by
    apply tendsto_zero_of_abs_tendsto_zero
    simp_rw [abs_mul]
    apply tendsto_zero_of_abs_le_tendsto_zero (fun x ↦ |log x| * |x| ^ r)
    intro x
    simp
    have : abs (fun x => |log x| * |(-x) ^ r|) x = |log x| * |(-x) ^ r| := by
        have abs_fun_applied (f: ℝ → ℝ) (x : ℝ) : abs f x = |f x| := rfl
        rw [abs_fun_applied (fun x => |log x| * |(-x) ^ r|) x]
        simp
        rw [←abs_mul]
        exact abs_nonneg (log x * (-x) ^ r)
    rw [this]
    · gcongr
      rw [show |x| = |-x| by simp]
      apply Real.abs_rpow_le_abs_rpow
    · convert (tendsto_log_mul_rpow_nhds_zero hr).norm.congr' ?_
      · simp
      · filter_upwards [self_mem_nhdsWithin] with x hx
        simp_rw [norm_mul, norm_rpow_of_nonneg (mem_Ioi.mp hx).le, norm_eq_abs]

/-- This is a direct generalization of `tendsto_log_mul_rpow_nhds_zero`
(replaces `>` by `≥`) -/
lemma tendsto_log_mul_rpow_nhds_zero' {r : ℝ} (hr : 0 < r) :
    Tendsto (fun x => log x * x ^ r) (𝓝[≥] 0) (𝓝 0) := by
        apply tendsto_ge_of_tendsto_gt_funvalue
        apply tendsto_log_mul_rpow_nhds_zero
        exact hr
        norm_num

/-- This is a generalization of `tendsto_log_mul_rpow_nhds_zero`
(replaces `ndhdsWithin` by `nhds`) -/
lemma tendsto_log_mul_rpow_nhds_zero'' {r : ℝ} (hr : 0 < r) :
    Tendsto (fun x => log x * x ^ r) (𝓝 0) (𝓝 0) := by
        have union_tozero_fromzero : Iio (0 : ℝ) ∪ Ici 0 = univ := by simp
        refine tendsto_of_union_tendstoWithin union_tozero_fromzero ?_ ?_
        · apply tendsto_nhdsWithin_of_tendsto_nhdsWithin_neg.mpr
          convert tendsto_rpow_neg hr using 1
          simp
        exact tendsto_log_mul_rpow_nhds_zero' hr

lemma continuousAt_zero_log_mul_rpow {r : ℝ} (hr : 0 < r)
: ContinuousAt (fun (x : ℝ) ↦ log x * x ^ r) 0 := by
    apply continuousAt_of_tendsto_nhds (y:=0)
    exact tendsto_log_mul_rpow_nhds_zero'' hr

/--
In Mathlib, the Real natural logarithm is defined as `log |⬝|` (and zero at zero).
Real powers are defined such that
    · For `x > 0`, `x ^ y = exp (y log x)`.
    · For `x < 0`, `x ^ y = exp (y log x) cos (π y)`

Together, this implies that for `r > 0` the funciton `x ↦ x^r * log x` is continuous over ℝ.
-/
lemma continuous_log_mul_rpow {r : ℝ} (hr : 0 < r)
: Continuous (fun (x : ℝ) ↦ log x * x ^ r) := by
    apply continuous_iff_continuousAt.mpr
    intro x
    by_cases h : x = 0
    · rw [h]
      exact continuousAt_zero_log_mul_rpow hr
    · apply ContinuousAt.mul
      apply ContinuousAt.log
      apply continuousAt_id
      apply h
      refine continuousAt_rpow_const x r ?_
      left; assumption

end XLogX

[Yongyi Chen]

Good practice for me! I got it down to 43 lines, not quite the 10x reduction you were looking for but here you go.

import Mathlib.Analysis.SpecialFunctions.Pow.Continuity

open Filter Topology Real

lemma neg_nhds_right_eq_nhds_left : (𝓝[>] (0 : ℝ)).map Neg.neg = 𝓝[<] 0 := by
  rw [nhdsWithin, Filter.map_inf neg_injective, map_principal, Set.image_neg_Ioi, neg_zero]
  congr 1
  exact nhds_zero_symm' ℝ

lemma neg_nhds_left_eq_nhds_right : (𝓝[<] (0 : ℝ)).map Neg.neg = 𝓝[>] 0 := by
  rw [nhdsWithin, Filter.map_inf neg_injective, map_principal, Set.image_neg_Iio, neg_zero]
  congr 1
  exact nhds_zero_symm' ℝ

lemma tendsto_nhdsWithin_iff_neg {f : ℝ → ℝ} : (𝓝[<] 0).Tendsto f (𝓝 a) ↔ (𝓝[>] 0).Tendsto (fun x => f (-x)) (𝓝 a) := by
  constructor <;> intro h
  . exact h.comp (le_of_eq neg_nhds_right_eq_nhds_left)
  . suffices Tendsto (f ∘ Neg.neg ∘ Neg.neg) (𝓝[<] 0) (𝓝 a) by
      simpa only [neg_involutive, Function.Involutive.comp_self, Function.comp.right_id] using this
    exact h.comp (le_of_eq neg_nhds_left_eq_nhds_right)

lemma continuous_log_mul_rpow {r : ℝ} (hr : 0 < r) : Continuous (fun (x : ℝ) => log x * x ^ r) := by
  rw [continuous_iff_continuousAt]
  intro x
  by_cases h : x = 0
  . subst h
    rw [continuousAt_iff_continuous_left'_right', ContinuousWithinAt, ContinuousWithinAt]
    norm_num
    constructor
    . simp only [tendsto_nhdsWithin_iff_neg, log_neg_eq_log]
      have bound : ∀ x > 0, ‖log x * (-x) ^ r‖ ≤ |log x| * |x ^ r| := by
        intro x xpos
        simp [norm_mul, norm_eq_abs, gt_iff_lt, abs_pos, ne_eq, log_eq_zero, abs_of_pos (rpow_pos_of_pos xpos r)]
        gcongr
        nth_rw 2 [← abs_of_pos xpos]
        rw [← abs_neg x]
        exact abs_rpow_le_abs_rpow _ _
      apply squeeze_zero_norm' (eventually_nhdsWithin_of_forall bound)
      simp only [← norm_eq_abs, ← norm_mul, ← tendsto_zero_iff_norm_tendsto_zero]
      exact tendsto_log_mul_rpow_nhds_zero hr
    . exact tendsto_log_mul_rpow_nhds_zero hr
  . push_neg at h
    exact Real.continuousAt_log h |>.mul (Real.continuousAt_rpow_const _ _ (Or.inl h))

[Jireh Loreaux]

I played with this a bit, but not too much:

import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics

open Filter Topology Real Asymptotics Bornology

lemma isLittleO_log_rpow_cobounded {r : ℝ} (hr : 0 < r) :
    log =o[cobounded ℝ] fun x => ‖x‖ ^ r := by
  rw [Real.cobounded_eq, isLittleO_sup]
  have := calc
    log =o[atTop] (· ^ r) := isLittleO_log_rpow_atTop hr
    _   =ᶠ[atTop] (‖·‖ ^ r) := by
      filter_upwards [Ici_mem_atTop 0] with x (hx : 0 ≤ x) using by rw [norm_of_nonneg hx]
  refine ⟨?_, this⟩
  convert this.comp_tendsto tendsto_neg_atBot_atTop using 1
  all_goals apply funext; simp

lemma norm_rpow_le {x y : ℝ} : ‖x ^ y‖ ≤ ‖x‖ ^ y := by
  obtain (hx|hx) := lt_or_le x 0
  · rw [rpow_def_of_neg hx, rpow_def_of_pos (norm_pos_iff.mpr hx.ne)]
    simpa only [norm_mul, norm_eq_abs, abs_exp, log_abs, mul_le_iff_le_one_right (exp_pos _)]
      using abs_cos_le_one (y * π)
  · exact (norm_rpow_of_nonneg hx).le

theorem Real.tendsto_log_cobounded : Tendsto log (cobounded ℝ) atTop := by
  rw [Real.cobounded_eq, tendsto_sup]
  refine ⟨?_, tendsto_log_atTop⟩
  convert Real.tendsto_log_atTop.comp tendsto_neg_atBot_atTop
  funext
  simp [Function.comp_apply]

[Adomas Baliuka]

@Jireh Loreaux that's not "garbage values" though, is it? I'm a bit surprised (assuming what I just learned about Bornology was right) this wasn't in Mathlib yet. (Also, the Bornology pages would definitely benefit from more docs. A lot of people don't learn about bornology, same as filters. How about adding "used e.g. to talk about limits towards infinity" to cobounded docs?)

[Kevin Buzzard]

Please feel free to make docstring PRs! If you see something in mathlib which could be better, you can just make it better and people are very receptive to this approach.

[Jireh Loreaux]

You can use it to get the version you want with a bit more work. Note that docs#isLittleO_log_rpow_atTop is the first step toward proving the existing log mul rpow result.

[Jireh Loreaux]

You're welcome to PR anything I wrote if you feel like it.