proving 2^x is continous

Stream: new members

[Sabbir Rahman]

How to prove simply that fun (x: ℝ) => (2:ℝ)^x is continuous? Given how fundamental it seems I think there should be one-liner or two-liner for this, but can't seem to find relevant theorems

[Yakov Pechersky]

docs#Real.continuousAt_const_rpow

[Yakov Pechersky]

import Mathlib

lemma Real.continuous_const_rpow {a : ℝ} (ha : a ≠ 0) :
    Continuous (fun x : ℝ ↦ a ^ x) := by
  rw [continuous_iff_continuousOn_univ]
  refine continuousOn_of_forall_continuousAt ?_
  exact fun _ _ ↦ continuousAt_const_rpow ha

[Michael Stoll]

I would expect fun_prop to do this, but apparently it doesn't ...

import Mathlib

/-
`fun_prop` was unable to prove `Continuous fun x => 2 ^ x`
-/
example : Continuous fun x : ℝ ↦ (2 : ℝ) ^ x := by fun_prop

[Michael Stoll]

It looks like some fun_prop attributes are missing.

import Mathlib

@[fun_prop]
lemma Real.continuous_const_rpow {a : ℝ} (ha : a ≠ 0) :
    Continuous (fun x : ℝ ↦ a ^ x) := by
  rw [continuous_iff_continuousOn_univ]
  refine continuousOn_of_forall_continuousAt ?_
  exact fun _ _ ↦ continuousAt_const_rpow ha

/-
`fun_prop` was unable to prove `Continuous fun x => 2 ^ x`

Issues:
  Failed to prove necessary assumption `2 ≠ 0` when applying theorem `Real.continuous_const_rpow`.
-/
example : Continuous fun x : ℝ ↦ (2 : ℝ) ^ x := by fun_prop

[Michael Stoll]

This works:

import Mathlib

@[fun_prop]
lemma Real.continuous_const_rpow {a : ℝ} (ha : a ≠ 0) :
    Continuous (fun x : ℝ ↦ a ^ x) := by
  rw [continuous_iff_continuousOn_univ]
  refine continuousOn_of_forall_continuousAt ?_
  exact fun _ _ ↦ continuousAt_const_rpow ha

example : Continuous fun x : ℝ ↦ (2 : ℝ) ^ x := by fun_prop (disch := norm_num)

[Michael Stoll]

One can also try fun_prop (disch := hint), which suggests linarith.

[Sabbir Rahman]

I had seen the continuousAt_const_rpow and had also seen continous_const_cpow but didn’t find direct theorem akin to continuous_const_rpow I think it should be in mathlib, how can I raise a request or contribute to add this?

[Kevin Buzzard]

You can make a PR and add it yourself! Information on how to do this is on the community website (sorry for no precise link, on mobile right now) here.

[Tomas Skrivan]

Nice, I have never tried disch:=hint. I always run disch:=trace_state; sorry and look at the info view which subgoals were sorried and choose the appropriate tactic based on that.

[Isak Colboubrani]

That would be a nice contribution @Sabbir Rahman.

What about adding a @[continuity] annotation too? Then continuity will close this goal too:

import Mathlib

@[fun_prop, continuity]
lemma Real.continuous_const_rpow {a : ℝ} (ha : a ≠ 0) :
    Continuous (fun x : ℝ ↦ a ^ x) := by
  rw [continuous_iff_continuousOn_univ]
  refine continuousOn_of_forall_continuousAt ?_
  exact fun _ _ ↦ continuousAt_const_rpow ha

example : Continuous fun x : ℝ ↦ (2 : ℝ) ^ x := by continuity
example : Continuous fun x : ℝ ↦ (2 : ℝ) ^ x := by fun_prop (disch := norm_num)

[Eric Rodriguez]

continuity is all but discontinued afaik

[Isak Colboubrani]

I didn't know that. TIL!

Is this documented somewhere? Would a @[deprecated] annotation be appropriate?

[Michael Stoll]

Re: fun_prop, I'm surprised that the following does not work:

import Mathlib

example {f g : ℝ → ℝ} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
    Differentiable ℝ (f * g) := by
  fun_prop

[Kevin Buzzard]

import Mathlib

example {f g : ℝ → ℝ} (hf : Differentiable ℝ f) (hg : Differentiable ℝ g) :
    Differentiable ℝ (f * g) := by
  change Differentiable ℝ (fun x ↦ f x * g x)
  fun_prop

I think there's a long ongoing discussion about this sort of thing!

[Sabbir Rahman]

Created PR to add the lemma :raised_hands: