Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - fix(Analysis/../CompareExp): fix natural powers #7837

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - fix(Analysis/../CompareExp): fix natural powers #7837

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 20 additions & 21 deletions Mathlib/Analysis/SpecialFunctions/CompareExp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,8 +30,9 @@ stronger assumptions (e.g., `im z` is bounded from below and from above) are not


open Asymptotics Filter Function
open scoped Topology

open Topology
local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220

namespace Complex

Expand All @@ -55,7 +56,6 @@ variable {l : Filter ℂ}
### Alternative constructors
-/


theorem of_isBigO_im_re_rpow (hre : Tendsto re l atTop) (r : ℝ) (hr : im =O[l] fun z => z.re ^ r) :
IsExpCmpFilter l :=
⟨hre, fun n =>
Expand All @@ -71,15 +71,14 @@ set_option linter.uppercaseLean3 false in

theorem of_isBigO_im_re_pow (hre : Tendsto re l atTop) (n : ℕ) (hr : im =O[l] fun z => z.re ^ n) :
IsExpCmpFilter l :=
of_isBigO_im_re_rpow hre n <| by norm_cast at hr; simpa only [Real.rpow_nat_cast]
of_isBigO_im_re_rpow hre n <| by exact_mod_cast hr
set_option linter.uppercaseLean3 false in
#align complex.is_exp_cmp_filter.of_is_O_im_re_pow Complex.IsExpCmpFilter.of_isBigO_im_re_pow

theorem of_boundedUnder_abs_im (hre : Tendsto re l atTop)
(him : IsBoundedUnder (· ≤ ·) l fun z => |z.im|) : IsExpCmpFilter l :=
of_isBigO_im_re_pow hre 0 <| by
norm_cast
simpa only [pow_zero] using @IsBoundedUnder.isBigO_const ℂ ℝ ℝ _ _ _ l him 1 one_ne_zero
simpa only [pow_zero] using him.isBigO_const (f := im) one_ne_zero
#align complex.is_exp_cmp_filter.of_bounded_under_abs_im Complex.IsExpCmpFilter.of_boundedUnder_abs_im

theorem of_boundedUnder_im (hre : Tendsto re l atTop) (him_le : IsBoundedUnder (· ≤ ·) l im)
Expand All @@ -91,7 +90,6 @@ theorem of_boundedUnder_im (hre : Tendsto re l atTop) (him_le : IsBoundedUnder (
### Preliminary lemmas
-/


theorem eventually_ne (hl : IsExpCmpFilter l) : ∀ᶠ w : ℂ in l, w ≠ 0 :=
hl.tendsto_re.eventually_ne_atTop' _
#align complex.is_exp_cmp_filter.eventually_ne Complex.IsExpCmpFilter.eventually_ne
Expand All @@ -112,15 +110,12 @@ theorem isLittleO_im_pow_exp_re (hl : IsExpCmpFilter l) (n : ℕ) :
(fun z : ℂ => z.im ^ n) =o[l] fun z => Real.exp z.re :=
flip IsLittleO.of_pow two_ne_zero <|
calc
((fun z : ℂ => (z.im ^ n)) ^ 2) = (fun z : ℂ => (z.im ^ n) ^ 2) := funext <| by simp
_ = fun z => (Complex.im z) ^ (2 * n) := funext <| fun _ => by norm_cast; rw [pow_mul']
_ =O[l] fun z => Real.exp z.re := by have := hl.isBigO_im_pow_re (2 * n); norm_cast at *
_ = fun z => Real.exp z.re ^ 1 := funext <| fun _ => by norm_cast; rw [pow_one]
_ =o[l] fun z => Real.exp z.re ^ 2 := by
have := (isLittleO_pow_pow_atTop_of_lt one_lt_two).comp_tendsto <|
(fun z : ℂ ↦ (z.im ^ n) ^ 2) = (fun z ↦ z.im ^ (2 * n)) := by simp only [pow_mul']
_ =O[l] fun z ↦ Real.exp z.re := hl.isBigO_im_pow_re _
_ = fun z ↦ (Real.exp z.re) ^ 1 := by simp only [pow_one]
_ =o[l] fun z ↦ (Real.exp z.re) ^ 2 :=
(isLittleO_pow_pow_atTop_of_lt one_lt_two).comp_tendsto <|
Real.tendsto_exp_atTop.comp hl.tendsto_re
simpa only [pow_one, Real.rpow_one, Real.rpow_two]
_ = (fun z => Real.exp z.re) ^ 2 := funext <| by simp
#align complex.is_exp_cmp_filter.is_o_im_pow_exp_re Complex.IsExpCmpFilter.isLittleO_im_pow_exp_re

theorem abs_im_pow_eventuallyLE_exp_re (hl : IsExpCmpFilter l) (n : ℕ) :
Expand Down Expand Up @@ -164,22 +159,26 @@ theorem isLittleO_log_abs_re (hl : IsExpCmpFilter l) : (fun z => Real.log (abs z
### Main results
-/

lemma isTheta_cpow_exp_re_mul_log (hl : IsExpCmpFilter l) (a : ℂ) :
(· ^ a) =Θ[l] fun z ↦ Real.exp (re a * Real.log (abs z)) :=
calc
(fun z => z ^ a) =Θ[l] (fun z : ℂ => (abs z ^ re a)) :=
isTheta_cpow_const_rpow fun _ _ => hl.eventually_ne
_ =ᶠ[l] fun z => Real.exp (re a * Real.log (abs z)) :=
(hl.eventually_ne.mono fun z hz => by simp only [Real.rpow_def_of_pos, abs.pos hz, mul_comm])

/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a` and any
positive real `b`, we have `(fun z ↦ z ^ a) =o[l] (fun z ↦ exp (b * z))`. -/
theorem isLittleO_cpow_exp (hl : IsExpCmpFilter l) (a : ℂ) {b : ℝ} (hb : 0 < b) :
(fun z => z ^ a) =o[l] fun z => exp (b * z) :=
-- Porting note: Added `show ℂ → ℝ from`
calc
(fun z => z ^ a) =Θ[l] (show ℂ → ℝ from fun z => (abs z ^ re a)) :=
isTheta_cpow_const_rpow fun _ _ => hl.eventually_ne
_ =ᶠ[l] fun z => Real.exp (re a * Real.log (abs z)) :=
(hl.eventually_ne.mono fun z hz => by simp only [Real.rpow_def_of_pos, abs.pos hz, mul_comm])
(fun z => z ^ a) =Θ[l] fun z => Real.exp (re a * Real.log (abs z)) :=
hl.isTheta_cpow_exp_re_mul_log a
_ =o[l] fun z => exp (b * z) :=
IsLittleO.of_norm_right <| by
simp only [norm_eq_abs, abs_exp, ofReal_mul_re, Real.isLittleO_exp_comp_exp_comp]
refine'
(IsEquivalent.refl.sub_isLittleO _).symm.tendsto_atTop (hl.tendsto_re.const_mul_atTop hb)
refine (IsEquivalent.refl.sub_isLittleO ?_).symm.tendsto_atTop
(hl.tendsto_re.const_mul_atTop hb)
exact (hl.isLittleO_log_abs_re.const_mul_left _).const_mul_right hb.ne'
#align complex.is_exp_cmp_filter.is_o_cpow_exp Complex.IsExpCmpFilter.isLittleO_cpow_exp

Expand Down