Hi,
I would like to prove that for :
In Isabelle, this might look something like:
lemma
fixes a::real
assumes "a > 0"
shows "((λx. a ^ x) ⤏ 1) F"
what filter should I used for 'tends to zero from above' and is there a real power function that makes x real? In the above currently, Isabelle is inferring nat as the type for x.
This is part of a personal study to see how easy it is to do some basic limit problems in a nice and accessible way. Limit problems such as this one on Youtube.
Cheers
Mark
sorry, wrong thread
Funny you should ask, if you import HOL-Real_Asymp.Real_Asymp
, this goes through with using assms by real_asymp
. :smile:
And as for your other questions, x powr y
is the power function on real numbers (caveat: 0 ^ y = 0
for any y
and it's undefined for x < 0
) or complex numbers (same caveat for x = 0
, branch cut for negative real y
as usual).
The F
in your case should simply be at_right 0
. This is an abbreviation for at 0 within {0<..}
, and at x within A
is basically the neighbourhood filter nhds x
restricted to A - {x}
, i.e. you can approach x
from any ‘path’ within A-{x}
.
You can even prove something stronger, namely filterlim (λx. a powr x) (at_right 1) (at_right 0)
.
Correction: You need a case distinction over a < 1
, a = 1
and a > 1
though because real_asymp
works by computing series expansions and these look a bit different in each of these cases: without the case distinction, real_asymp
will tell you that it was unable to determine the sign of ln a
if you run it with real_asymp (verbose)
.
There is also the diagnostic tool real_limit
with which you can find the limit of an expression:
context
fixes a b :: real
assumes a: "a > 0" "a < 1" and b: "b > 1"
begin
real_limit "λx. a powr x"
limit: "at_right 0" facts: a
real_limit "λx. b powr x"
limit: "at_right 0" facts: b
For completeness, here the more detailed variant where you also show from where it approaches:
lemma "a ∈ {0<..<1} ⟹ filterlim (λx::real. a powr x) (at_left 1) (at_right 0)"
"a > 1 ⟹ filterlim (λx::real. a powr x) (at_right 1) (at_right 0)"
by real_asymp+
The video you posted shows the example . The problem with that is that for technical reasons, real_asymp
currently does not support root n x
where n
is not a constant. However, you can prove a more general version like this:
lemma
fixes a b :: real
assumes "a > 0" "b > 0"
shows "((λx. ((a powr (1/x) + b powr (1/x)) / 2) powr x) ⤏ exp ((ln a + ln b) / 2)) at_top"
using assms by real_asymp
There is also documentation for real_asymp
in ~~/Doc/Real_Asymp
. And you can of course always ask me if you have any questions!
Addendum: here is a proof of your initial question without real_asymp
, using the continuity of powr
at 0
:
lemma
fixes a::real
assumes "a > 0"
shows "((λx. a powr x) ⤏ 1) (at_right 0)"
proof -
from assms have "((λx. a powr x) ⤏ a powr 0) (nhds 0)"
by (intro tendsto_intros filterlim_ident) auto
hence "((λx. a powr x) ⤏ a powr 0) (at_right 0)"
by (rule filterlim_mono) (auto simp: at_within_le_nhds)
thus ?thesis using assms by simp
qed
This uses the rule tendsto_powr'
, which is in the tendsto_intros
collection:
(f ⤏ a) F ⟹ (g ⤏ b) F ⟹ a ≠ 0 ∨ 0 < b ∧ (∀⇩F x in F. 0 ≤ f x)
⟹ ((λx. f x powr g x) ⤏ a powr b) F
These proofs get fairly tedious for more complicated limits though – which is why I made real_asymp
. See this paper for a description of how it works if you're curious (but for instructions on how to use it, look at the documentation instead or ask me).
Wonderful. Thank you.
Last updated: Dec 07 2024 at 16:22 UTC