Proving `¬ DifferentiableAt`

Stream: new members

[Adomas Baliuka]

I'm trying to remove assumptions from lemmas about deriv. For example, deriv2_negMulLog (which says that the second derivative of $-x \log x$ is $- 1/x$) has an assumption that x ≠ 0. This assumption is unnecessary because both sides of the equation take a junk value at 0. To remove the assumption, I need to prove that the function is ¬ DifferentiableAt there.

There's a few lemmas that prove such things but I don't see how to adapt the approaches there. For example,not_differentiableAt_abs_zero uses the fact that abs equals -x or x near 0. I was wondering how you would approach these, for example (assuming they're true)?

/- Can be generalized-/
lemma not_differentiableAt_of_tendsto_atTop (f : ℝ → ℝ) (x : ℝ)
    (h : Tendsto |f| (𝓝[>] x) atTop) :
    ¬ DifferentiableAt ℝ f x := by sorry

/- Can be generalized-/
lemma not_differentiableAt_of_deriv_tendsto_atTop (f : ℝ → ℝ) (x : ℝ)
    (h : Tendsto |deriv f| (𝓝[>] x) atTop) :
    ¬ DifferentiableAt ℝ f x := by sorry

In the case of deriv2_negMulLog, I can use the approach from differentiableAt_log_iff which uses non-continuity. However, in general having more lemmas that help prove ¬ DifferentiableAt might be useful?

[Adomas Baliuka]

In trying to do this, I find it really hard to deal with filters. How can I prove that the range of a function that tends to infinity is unbounded? After some Loogle searches I seem to be missing a big chunk of API that I would expect to be there. The most relevant thing I found so far was Metric.tendsto_dist_left_atTop_iff.

I guess the underlying problem for me (as a non-mathematician who mostly cares about stuff building on real/complex numbers) suddenly having to deal with filters and bornology that are actually used for everything is overwhelming. Any advice?

import Mathlib
open Filter

lemma exists_upperBound_of_tendsto_atTop (f : ℝ → ℝ) (l : Filter ℝ)
    (h : Tendsto f l atTop) :
    ∀ C, ∃ x, C < f x := sorry

[Yury G. Kudryashov]

You also need [Nebot l]

[Yury G. Kudryashov]

Then you can use (h.eventually_gt_atTop C).exists

[Adomas Baliuka]

Thanks a lot! Any general advice on how to find such things? I'm still struggling to solve even very similar problems to this one :(

import Mathlib
open Real Topology Filter
lemma exists_upperBound_of_tendsto_atTop {f : ℝ → ℝ} {l : Filter ℝ} [NeBot l]
    (h : Tendsto f l atTop) :
    ∀ C, ∃ x, C < f x := fun _ ↦ (h.eventually_gt_atTop _).exists

/-- Given `C : ℝ`, if a function `f` diverges when approaching a point `x` from above,
there is a point `x2` in any neighborhood of x such that `C ≤ |f x2 - f x|`.  -/
lemma exists_upperBound_of_tendsto_nhdsWithin_atTop {f : ℝ → ℝ} {x : ℝ}
    (h : Tendsto f (𝓝[>] x) atTop) :
    ∀ C, ∀ δ>0, ∃ x2, |x2 - x| < δ ∧ C ≤ |f x2 - f x| := by
  intro C δ hδ
  sorry

Is there a characterization (an Iff lemma) of what Tendsto f (𝓝[>] x) atTop means for functions Real -> Real in terms of epsilon-delta?
Loogle for Filter.Tendsto _ (nhdsWithin _ _) Filter.atTop does not find anything useful...

I intend to use the above to do things like this:

lemma not_continuousAt_of_deriv_tendsto_atTop (f : ℝ → ℝ) (x : ℝ)
    (h : Tendsto f (𝓝[>] x) atTop) :
    ¬ ContinuousAt f x := by
  intro contAt
  have epsdelta := Metric.continuousAt_iff.mp contAt
  suffices : ¬∀ ε > 0, ∃ δ > 0, ∀ {x_1 : ℝ}, dist x_1 x < δ → dist (f x_1) (f x) < ε
  · contradiction
  · push_neg
    use 1
    constructor
    exact Real.zero_lt_one
    intro δ hδ
    simp [dist]
    exact exists_upperBound_of_tendsto_nhdsWithin_atTop h 1 δ hδ

[Adomas Baliuka]

For my PR defining binary entropy, I now tried to directly prove ¬ DifferentiableAt ℝ (fun x => x * log x) 0 using filters. I "reduced" it to ∃ᶠ (x : ℝ) in nhds 0, |x| < |x| * |x.log - deriv (fun y ↦ y * y.log) 0|. The deriv (...) 0 : ℝ part is irrelevant, since the claim is true for any real number (because it cannot depend on x).

My informal argument would now be that

It suffices to show that for any given real number D (that's the deriv (...)) and any epsilon > 0 (sufficient to show existance in any arbitrarily small neighborhood since any such contains an open ball) there exists an x with |x| < epsilon such that |x| < |x| * |x.log - D|. Since |log x| grows without bound when approaching zero (say, from above), there always exists such an x. One could take, if one needed to be explicit e.g., x := 1/2 * min (exp (D + 1)) epsilon

How to do this in Lean? I loogle'd |- Filter.Frequently _ (nhds _) and found little, none of which seemed useful. In general, it would be really nice to have epsilon-delta characterizations for metric spaces of these filter statements with nhds.

Just in case anyone is interested, the "rest" of my argument for non-differentiability is

import Mathlib

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]

@[simp]
theorem fderiv_deriv' {f : 𝕜 → 𝕜} {x y : 𝕜} : (fderiv 𝕜 f x : 𝕜 → 𝕜) y = (deriv f x) * y := by
  rw [← deriv_fderiv]
  simp
  ring

lemma not_DifferentiableAt_log_mul_zero : ¬ DifferentiableAt ℝ (fun x => x * log x) 0 := by
  intro h
  have := DifferentiableAt.hasFDerivAt h
  have := hasFDerivAt_iff_isLittleO_nhds_zero.mp this
  simp at this
  have := Asymptotics.IsLittleO.bound this
  have myCalc (x : ℝ) : x * x.log - deriv (fun x ↦ x * x.log) 0 * x
    = x * (x.log - deriv (fun x ↦ x * x.log) 0 ) := by ring
  simp only [myCalc, norm_mul, norm_eq_abs] at this
  have := @this 1 (by norm_num)
  simp only [one_mul] at this
  have contr : ¬ ∀ᶠ (x : ℝ) in nhds 0, |x| * |x.log - deriv (fun x ↦ x * x.log) 0| ≤ |x| := by
    apply Filter.not_eventually.mpr
    simp
    sorry
  contradiction

[Frédéric Dupuis]

I haven't gone through the full argument, but I would try something like this:

open Real Filter in
example (f : ℝ → ℝ) : ¬ DifferentiableAt ℝ f 0 := by
  intro h
  have h₁ : (fun z => z) =o[𝓝[>] 0] fun z => f z - f 0 - deriv f 0 :=
    -- from the fact that the derivative blows up at zero
    sorry
  have h₂ : (fun z => f z - f 0 - deriv f 0) =o[𝓝[>] 0] fun z => z :=
    -- from the fact that it's differentiable at zero
    sorry
  -- Now get a contradiction
  have htrans := h₁.trans h₂
  refine Asymptotics.isLittleO_irrefl ?_ htrans
  refine Eventually.frequently ?_
  refine eventually_nhdsWithin_of_forall <| fun x hx => Ne.symm <| ne_of_lt hx

[Adomas Baliuka]

Thanks for the hint. Unfortunately, I couldn't figure it out how to prove the first have from "the derivative blowing up" because the derivative isn't used (except evaluated at zero, for which behavior around zero doesn't seem to matter?)

I managed to prove it by continuing my own "path" using explicit epsilon-delta. It's some of the ugliest code I've seen (and I'm an experimental physicist - believe me, I've seen some ugly code...) so I'm not sure if it's viable to use this in the PR (even if I managed to shorten it without completely changing the approach)?

import Mathlib

open Filter Real Topology Asymptotics

theorem extracted_1 (D x : ℝ): 0 < x → |min (2⁻¹ * x) (rexp (D - 2))| < x := by
  intro h
  have xhalf_lt_x : 2⁻¹ * x < x := by
    simp_all only [gt_iff_lt, mul_lt_iff_lt_one_left]
    norm_num
  by_cases xlt : 2⁻¹ * x < rexp (D - 2)
  · calc |min (2⁻¹ * x) (rexp (D - 2))|
      _ = |2⁻¹ * x| := by rw [min_eq_left_of_lt xlt]
      _ = 2⁻¹ * x := by
        simp only [abs_eq_self, gt_iff_lt, inv_pos, Nat.ofNat_pos, mul_nonneg_iff_of_pos_left,
          le_of_lt h]
      _ < x := xhalf_lt_x
  · calc |min (2⁻¹ * x) (rexp (D - 2))|
      _ = |rexp (D - 2)| := by
       simp_all only [gt_iff_lt, not_lt, ge_iff_le, min_eq_right, abs_exp]
      _ = rexp (D - 2) := by
        simp only [one_div, abs_eq_self, gt_iff_lt, inv_pos, Nat.ofNat_pos,
          mul_nonneg_iff_of_pos_left, exp_nonneg (D - 2)]
      _ < x := by linarith

theorem extracted_2 (x D : ℝ) (hx : 0 < x) (h : x < rexp (D - 2)) :
    1 < |x.log - D| := by
  have h := log_lt_log hx h
  simp at h
  by_cases abs_eq : x.log - D < 0
  · rw [abs_of_neg]
    have : x.log - D < -2 := sub_left_lt_of_lt_add h
    linarith
    exact abs_eq
  · rw [abs_of_pos]
    linarith
    have : x.log < D := by linarith
    linarith

lemma not_DifferentiableAt_log_mul_zero :
    ¬ DifferentiableAt ℝ (fun (x : Real) => x * log x) (0 : Real) := by
  intro h
  have := hasDerivAt_iff_isLittleO_nhds_zero.mp (DifferentiableAt.hasDerivAt h)
  simp only [zero_add, log_zero, mul_zero, sub_zero, smul_eq_mul] at this
  have := Asymptotics.IsLittleO.bound this
  have myCalc (x : ℝ) : x * x.log - deriv (fun x ↦ x * x.log) 0 * x
    = x * (x.log - deriv (fun x ↦ x * x.log) 0 ) := by ring
  simp only [myCalc, norm_mul, norm_eq_abs] at this
  have := @this 1 (by norm_num)
  simp only [one_mul] at this
  have contr : ¬ ∀ᶠ (x : ℝ) in 𝓝 0, |x * x.log - x * deriv (fun x ↦ x * x.log) 0| ≤ |x|:= by
    let D := (deriv (fun x ↦ x * x.log) (0 : ℝ))
    rw [← show D = (deriv (fun x ↦ x * x.log) (0 : ℝ)) by rfl]
    simp [eventually_nhdsWithin_iff, Metric.eventually_nhds_iff]
    intro x hx
    exists (min (2⁻¹ * x) (exp (D - 2)))
    have xhalf_gt0 : 0 < 2⁻¹ * x := by
      simp_all only [differentiableAt_id', gt_iff_lt, mul_lt_iff_lt_one_left, inv_pos, Nat.ofNat_pos,
        mul_pos_iff_of_pos_left]
    constructor
    · exact extracted_1 D x hx
    · have exists_pos : 0 < |min (2⁻¹ * x) (rexp (D - 2))| := by
        simp only [one_div, abs_pos, ne_eq, mul_eq_zero, inv_eq_zero, OfNat.ofNat_ne_zero, false_or]
        exact ne_of_gt (lt_min xhalf_gt0 (exp_pos (D - 2)))
      have calcc := calc
          |min (2⁻¹ * x) (rexp (D - 2)) * (min (2⁻¹ * x) (rexp (D - 2))).log - min (2⁻¹ * x) (rexp (D - 2)) * D|
          _ = |(min (2⁻¹ * x) (rexp (D - 2))) * ((min (2⁻¹ * x) (rexp (D - 2))).log - D)| := by ring_nf
          _ = |min (2⁻¹ * x) (rexp (D - 2))| * |(min (2⁻¹ * x) (rexp (D - 2))).log - D| := by
            simp only [one_div, abs_mul]
      rw [calcc]
      apply (lt_mul_iff_one_lt_right exists_pos).mpr
      by_cases min_l : (2⁻¹ * x) < (rexp (D - 2))
      · rw [min_eq_left_of_lt min_l]
        exact extracted_2 (2⁻¹ * x) D xhalf_gt0 min_l
      · rw [min_eq_right (le_of_not_lt min_l)]
        simp only [log_exp, sub_sub_cancel_left, abs_neg, Nat.abs_ofNat, Nat.one_lt_ofNat]
  contradiction