Zulip Chat Archive
Stream: Is there code for X?
Topic: Asymptotics conversions from equivalents
Ryan Lahfa (Aug 18 2021 at 15:04):
I'm looking at the asymptotics API to prove that when , and it seems like there is no theorem to convert an equivalent to an is_o
relation.
What I'm looking for is, if , proving is equivalent to proving .
Is there a nice way to do it or should there be a convert theorem (that I might have missed)?
Here's a MWE to illustrate what I'm trying to do:
import analysis.special_functions.exp_log
import analysis.asymptotics.asymptotic_equivalent
import analysis.asymptotics.asymptotics
open filter
open_locale asymptotics topological_space
lemma asymptotics.is_equivalent.left_comp_log {f g: ℝ → ℝ} {l: filter ℝ}
(h: f ~[l] g) (htop: tendsto f l at_top): real.log ∘ f ~[l] real.log ∘ g := sorry
lemma tendsto_log1_plus_x_under_x_at_top_nhds_1:
tendsto (λ (x: ℝ), real.log (1 + x) / x) at_top (𝓝 0) :=
begin
have h: tendsto (λ (x : ℝ), 1 + x) at_top at_top,
from tendsto_at_top_mono (by simp [zero_le_one]) (tendsto_id),
suffices : asymptotics.is_o real.log id at_top,
{
apply asymptotics.is_o.tendsto_0,
-- here I would like to prove log(x) = o(x) is enough to prove log(1 + x) = o(x) knowing log(1 + x) ~ log(x) by left_comp_log.
sorry,
},
have : asymptotics.is_o id real.exp at_top := sorry,
convert asymptotics.is_o.comp_tendsto this real.tendsto_log_at_top using 1,
ext, simp,
sorry,
end
Anatole Dedecker (Aug 18 2021 at 16:29):
I'm afraid this lemma doesn't exist, but it definitely should. I can't do Lean right now, but I think you should be able to get it by saying that u - v = o(v) = o(g)
since v = o(g)
(docs#asymptotics.is_o.trans), which then implies u = u - v + v = o(g)
(docs#asymptotics.is_o.add)
Ryan Lahfa (Aug 18 2021 at 16:49):
Anatole Dedecker said:
I'm afraid this lemma doesn't exist, but it definitely should. I can't do Lean right now, but I think you should be able to get it by saying that
u - v = o(v) = o(g)
sincev = o(g)
(docs#asymptotics.is_o.trans), which then impliesu = u - v + v = o(g)
(docs#asymptotics.is_o.add)
Thanks!
Ryan Lahfa (Aug 18 2021 at 17:52):
FWIW, here's the proof:
lemma asymptotics.is_equivalent_is_o_of_equivalent_of_o {u v w: ℝ → ℝ} {l: filter ℝ}
(h_equiv: u ~[l] v) (ho: is_o v w l): is_o u w l :=
begin
convert is_o.add (is_o.trans h_equiv ho) ho,
simp,
end
Ryan Lahfa (Aug 18 2021 at 18:45):
Enjoy the final proof:
import analysis.special_functions.exp_log
import analysis.asymptotics.asymptotic_equivalent
import analysis.asymptotics.asymptotics
import analysis.asymptotics.specific_asymptotics
open filter asymptotics
open_locale asymptotics topological_space
lemma eventually_nonzero_of_tendsto_at_top {f: ℝ → ℝ} {l: filter ℝ}
(htop: tendsto f l at_top): ∀ᶠ x in l, f x ≠ 0 :=
begin
have: ∀ᶠ (y: ℝ) in at_top, y ≠ 0,
{
simp [eventually_at_top],
exact ⟨ 1, λ b hb, by linarith only [hb] ⟩,
},
convert tendsto.eventually htop this,
end
lemma eventually_false_of_not {α} {p q: α → Prop} {l: filter α}
(hnp: ∀ᶠ x in l, ¬ p x): (∀ᶠ x in l, p x → q x) :=
eventually.mono hnp (λ x hnpx hpx, absurd hpx hnpx)
lemma asymptotics.is_o.of_tendsto_at_top {f: ℝ → ℝ} {l: filter ℝ}
(htop: tendsto f l at_top): is_o (1: ℝ → ℝ) f l :=
begin
refine (asymptotics.is_o_iff_tendsto' _).2 _,
exact eventually_false_of_not (eventually_nonzero_of_tendsto_at_top htop),
convert tendsto.inv_tendsto_at_top htop,
ext, simp,
end
lemma asymptotics.is_equivalent.left_comp_log {f g: ℝ → ℝ} {l: filter ℝ}
(h: f ~[l] g) (htop: tendsto f l at_top): real.log ∘ f ~[l] real.log ∘ g :=
begin
have fact1 : is_o (real.log ∘ f - real.log ∘ g) (1: ℝ → ℝ) l,
{
have hnonvanish: ∀ᶠ x in l, g x ≠ 0 := (eventually_nonzero_of_tendsto_at_top (is_equivalent.tendsto_at_top h htop)),
refine (asymptotics.is_o_iff_tendsto _).2 _,
simp only [forall_false_left, forall_const, pi.one_apply, one_ne_zero],
simp only [function.comp_app, pi.one_apply, div_one, pi.sub_apply],
refine tendsto.congr'
(_: real.log ∘ (f / g) =ᶠ[l] (λ (x: ℝ), real.log (f x) - real.log (g x))) _,
convert eventually.mono _ (λ (x: ℝ) (hx: f x ≠ 0 ∧ g x ≠ 0), @real.log_div (f x) (g x) hx.1 hx.2),
exact (eventually_nonzero_of_tendsto_at_top htop).and hnonvanish,
convert (real.continuous_at_log _).tendsto.comp
((is_equivalent_iff_tendsto_one hnonvanish).1 h),
all_goals { simp, },
},
have fact2 : is_o 1 (real.log ∘ g) l :=
asymptotics.is_o.of_tendsto_at_top
(real.tendsto_log_at_top.comp
((asymptotics.is_equivalent.tendsto_at_top_iff h).1 htop)),
exact is_o.trans fact1 fact2,
end
lemma asymptotics.is_equivalent.left_comp_log' {f g: ℝ → ℝ} {l: filter ℝ}
(h: f ~[l] g) (htop: tendsto g l at_top): real.log ∘ f ~[l] real.log ∘ g :=
asymptotics.is_equivalent.left_comp_log h ((asymptotics.is_equivalent.tendsto_at_top_iff h).2 htop)
lemma asymptotics.is_equivalent.is_o_of_equivalent_of_o {u v w: ℝ → ℝ} {l: filter ℝ}
(h_equiv: u ~[l] v) (ho: is_o v w l): is_o u w l :=
begin
convert is_o.add (is_o.trans h_equiv ho) ho,
simp,
end
lemma log_is_o_of_id:
is_o real.log id at_top :=
begin
refine asymptotics.is_o.congr'
(_: id ∘ real.log =ᶠ[at_top] real.log)
(_: real.exp ∘ real.log =ᶠ[at_top] id) _,
simp,
{
refine eventually.mono _ (λ (x: ℝ) (hx: 0 < x), real.exp_log hx),
rw [eventually_at_top],
exact ⟨ 1, λ a ha, by linarith [ha] ⟩,
},
{
refine asymptotics.is_o.comp_tendsto
_ real.tendsto_log_at_top,
refine
(asymptotics.is_o_iff_tendsto'
(eventually_false_of_not (eventually_of_forall real.exp_ne_zero))).2
_,
convert real.tendsto_pow_mul_exp_neg_at_top_nhds_0 1,
field_simp [real.exp_neg],
}
end
lemma tendsto_log1_plus_x_under_x_at_top_nhds_1:
tendsto (λ (x: ℝ), real.log (1 + x) / x) at_top (𝓝 0) :=
begin
suffices : asymptotics.is_o real.log id at_top,
{
apply asymptotics.is_o.tendsto_0,
refine
asymptotics.is_equivalent.is_o_of_equivalent_of_o
(_: (λ (x: ℝ), real.log (1 + x)) ~[at_top] real.log) this,
convert
asymptotics.is_equivalent.left_comp_log'
(_: (λ (x: ℝ), 1 + x) ~[at_top] id) tendsto_id,
convert (asymptotics.is_equivalent.refl).add_is_o _,
convert asymptotics.is_o_pow_pow_at_top_of_lt zero_lt_one,
simp,
exactI real.order_topology, -- why is this needed?
},
exact log_is_o_of_id,
end
I find it strange that I need to do exactI real.order_topology
but I'm super happy with the result :-) (the original proof involved to prove L'Hopital Rule + derivatives stuff for logs for +∞/+∞ and it was getting too messy.)
Patrick Massot (Aug 18 2021 at 18:48):
The I
in exactI
can't be needed. It means "please put something in the type class game for later use" while there is no later tactic there.
Patrick Massot (Aug 18 2021 at 18:48):
Presumably one of the tactic does instance search too late (apply
is very prone to do that, and I guess convert
can do it too) and you could simply use apply_instance
instead of exactI
.
Ryan Lahfa (Aug 18 2021 at 18:59):
Makes sense, then, thanks!
Anatole Dedecker (Aug 18 2021 at 19:37):
I think at some point I had an epsilon-delta proof of L'Hôpital's rule +∞/+∞ but it was extremely long and boring so I just didn't have the energy to turn it into a PR
Patrick Massot (Aug 18 2021 at 19:43):
I'm sure you can improve Ryan's proof, filling in missing mathlib lemmas along the way.
Mario Carneiro (Aug 18 2021 at 19:45):
Patrick Massot said:
The
I
inexactI
can't be needed. It means "please put something in the type class game for later use" while there is no later tactic there.
Actually that's the case with intro-like tactics, but for exact-like tactics the typeclass context is adjusted before the call to exact. exactI e
means "use all instances in the local context to elaborate e
and use it to finish the goal"
Patrick Massot (Aug 18 2021 at 19:55):
Yes, I thought about this during dinner.
Anatole Dedecker (Aug 18 2021 at 23:03):
This took way longer than expected because I wanted to make everything PR-ready (and also because I'm starting to be really tired), but here it is :
import analysis.special_functions.exp_log
import analysis.asymptotics.asymptotic_equivalent
import analysis.asymptotics.asymptotics
import analysis.asymptotics.specific_asymptotics
open filter asymptotics
open_locale asymptotics topological_space
--to mathlib
lemma eventually_ne_at_top {α : Type*} [preorder α] [no_top_order α] (a : α) :
∀ᶠ x in at_top, x ≠ a :=
(eventually_gt_at_top a).mono (λ x hx, hx.ne.symm)
--to mathlib (maybe rename is_o_one_iff ?)
lemma asymptotics.is_o_one_iff_left {α 𝕂 E : Type*} [normed_field 𝕂] [normed_group E] {f : α → E}
{l : filter α} : is_o (1 : α → 𝕂) f l ↔ tendsto (λ x, ∥f x∥) l at_top :=
begin
change is_o (λ _, 1 : α → 𝕂) f l ↔ _,
refine ⟨λ h, _, λ h, _⟩,
{ rw (at_top_basis' (1 : ℝ)).tendsto_right_iff,
intros c hc,
have : 0 < c := zero_lt_one.trans_le hc,
convert h.def (inv_pos.mpr this),
ext x,
rw [set.mem_Ici, norm_one, ← inv_mul_cancel (this.ne.symm),
mul_le_mul_left (inv_pos.mpr this)] },
{ rw is_o_iff,
intros c hc,
filter_upwards [h.eventually (eventually_ge_at_top c⁻¹)],
intros x hx,
rwa [norm_one, ← mul_inv_cancel (hc.ne.symm), mul_le_mul_left hc] }
end
-- to mathlib
lemma asymptotics.is_O_with.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂] {c : ℝ}
{l : filter α} {f g : α → 𝕂} (h : is_O_with c f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 :=
h.bound.mono (λ x hx hg, by simpa [hg] using hx)
-- to mathlib
lemma asymptotics.is_O.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂]
{l : filter α} {f g : α → 𝕂} (h : is_O f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 :=
let ⟨c, hc⟩ := h.is_O_with in hc.eventually_eq_zero_imp
-- to mathlib
-- TODO : `tendsto f l at_top` is too strong, `∀ᶠ x in l, ∥f x - 1∥ ≥ ε` should be enough
lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' {α : Type*} {f g : α → ℝ} {l : filter α}
(h : f ~[l] g) (htop : tendsto g l at_top) : real.log ∘ f ~[l] real.log ∘ g :=
begin
have hg : ∀ᶠ x in l, g x ≠ 0 := htop.eventually (eventually_ne_at_top 0),
have hf : ∀ᶠ x in l, f x ≠ 0 := hg.mp (h.symm.is_O.eventually_eq_zero_imp.mono (λ x, mt)),
have fact1 : is_o (real.log ∘ f - real.log ∘ g) (1 : α → ℝ) l,
{ refine (asymptotics.is_o_iff_tendsto (λ x (h : (1 : ℝ) = 0), (one_ne_zero h).elim)).2 _,
simp only [function.comp_app, pi.one_apply, div_one, pi.sub_apply],
have : tendsto (λ x, real.log (f x / g x)) l (𝓝 0) :=
real.log_one ▸ ((is_equivalent_iff_tendsto_one hg).mp h).log one_ne_zero,
refine this.congr' _,
filter_upwards [hf, hg] (λ x hfx hgx, real.log_div hfx hgx) },
have fact2 : is_o (1 : α → ℝ) (real.log ∘ g) l :=
asymptotics.is_o_one_iff_left.mpr (tendsto_norm_at_top_at_top.comp $
real.tendsto_log_at_top.comp htop),
exact is_o.trans fact1 fact2
end
-- to mathlib
lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top {α : Type*} {f g : α → ℝ}
{l : filter α} (h : f ~[l] g) (htop : tendsto f l at_top) :
real.log ∘ f ~[l] real.log ∘ g :=
asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' h (h.tendsto_at_top_iff.mp htop)
-- to mathlib
lemma asymptotics.is_o.congr_is_equivalent_left {α E : Type*} [normed_group E] {u v w : α → E}
{l: filter α} (ho: is_o v w l) (h_equiv: u ~[l] v) : is_o u w l :=
begin
convert is_o.add (is_o.trans h_equiv ho) ho,
simp,
end
-- to mathlib
lemma real.is_o_id_exp_at_top : is_o id real.exp at_top :=
begin
refine (asymptotics.is_o_iff_tendsto $ λ (x : ℝ) hx, (x.exp_pos.ne hx.symm).elim).mpr _,
convert real.tendsto_div_pow_mul_exp_add_at_top 1 0 1 zero_ne_one (le_refl _),
ext,
simp
end
-- to mathlib
lemma real.is_o_log_id_at_top:
is_o real.log id at_top :=
asymptotics.is_o.congr' (eventually_eq.refl _ _)
((eventually_gt_at_top 0).mono $ λ x hx, real.exp_log hx)
(real.is_o_id_exp_at_top.comp_tendsto real.tendsto_log_at_top)
lemma tendsto_log1_plus_x_under_x_at_top_nhds_0 :
tendsto (λ (x : ℝ), real.log (1 + x) / x) at_top (𝓝 0) :=
have this : 1 + id ~[at_top] id := (is_equivalent.refl).add_is_o
(asymptotics.is_o_one_iff_left.mpr tendsto_norm_at_top_at_top),
(real.is_o_log_id_at_top.congr_is_equivalent_left $
this.left_comp_log_of_tendsto_at_top' tendsto_id).tendsto_0
Ryan Lahfa (Aug 18 2021 at 23:07):
Anatole Dedecker said:
This took way longer than expected because I wanted to make everything PR-ready (and also because I'm starting to be really tired), but here it is :
import analysis.special_functions.exp_log import analysis.asymptotics.asymptotic_equivalent import analysis.asymptotics.asymptotics import analysis.asymptotics.specific_asymptotics open filter asymptotics open_locale asymptotics topological_space --to mathlib lemma eventually_ne_at_top {α : Type*} [preorder α] [no_top_order α] (a : α) : ∀ᶠ x in at_top, x ≠ a := (eventually_gt_at_top a).mono (λ x hx, hx.ne.symm) --to mathlib (maybe rename is_o_one_iff ?) lemma asymptotics.is_o_one_iff_left {α 𝕂 E : Type*} [normed_field 𝕂] [normed_group E] {f : α → E} {l : filter α} : is_o (1 : α → 𝕂) f l ↔ tendsto (λ x, ∥f x∥) l at_top := begin change is_o (λ _, 1 : α → 𝕂) f l ↔ _, refine ⟨λ h, _, λ h, _⟩, { rw (at_top_basis' (1 : ℝ)).tendsto_right_iff, intros c hc, have : 0 < c := zero_lt_one.trans_le hc, convert h.def (inv_pos.mpr this), ext x, rw [set.mem_Ici, norm_one, ← inv_mul_cancel (this.ne.symm), mul_le_mul_left (inv_pos.mpr this)] }, { rw is_o_iff, intros c hc, filter_upwards [h.eventually (eventually_ge_at_top c⁻¹)], intros x hx, rwa [norm_one, ← mul_inv_cancel (hc.ne.symm), mul_le_mul_left hc] } end -- to mathlib lemma asymptotics.is_O_with.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂] {c : ℝ} {l : filter α} {f g : α → 𝕂} (h : is_O_with c f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 := h.bound.mono (λ x hx hg, by simpa [hg] using hx) -- to mathlib lemma asymptotics.is_O.eventually_eq_zero_imp {α 𝕂 : Type*} [normed_field 𝕂] {l : filter α} {f g : α → 𝕂} (h : is_O f g l) : ∀ᶠ x in l, g x = 0 → f x = 0 := let ⟨c, hc⟩ := h.is_O_with in hc.eventually_eq_zero_imp -- to mathlib -- TODO : `tendsto f l at_top` is too strong, `∀ᶠ x in l, ∥f x - 1∥ ≥ ε` should be enough lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' {α : Type*} {f g : α → ℝ} {l : filter α} (h : f ~[l] g) (htop : tendsto g l at_top) : real.log ∘ f ~[l] real.log ∘ g := begin have hg : ∀ᶠ x in l, g x ≠ 0 := htop.eventually (eventually_ne_at_top 0), have hf : ∀ᶠ x in l, f x ≠ 0 := hg.mp (h.symm.is_O.eventually_eq_zero_imp.mono (λ x, mt)), have fact1 : is_o (real.log ∘ f - real.log ∘ g) (1 : α → ℝ) l, { refine (asymptotics.is_o_iff_tendsto (λ x (h : (1 : ℝ) = 0), (one_ne_zero h).elim)).2 _, simp only [function.comp_app, pi.one_apply, div_one, pi.sub_apply], have : tendsto (λ x, real.log (f x / g x)) l (𝓝 0) := real.log_one ▸ ((is_equivalent_iff_tendsto_one hg).mp h).log one_ne_zero, refine this.congr' _, filter_upwards [hf, hg] (λ x hfx hgx, real.log_div hfx hgx) }, have fact2 : is_o (1 : α → ℝ) (real.log ∘ g) l := asymptotics.is_o_one_iff_left.mpr (tendsto_norm_at_top_at_top.comp $ real.tendsto_log_at_top.comp htop), exact is_o.trans fact1 fact2 end -- to mathlib lemma asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top {f g: ℝ → ℝ} {l: filter ℝ} (h: f ~[l] g) (htop: tendsto f l at_top): real.log ∘ f ~[l] real.log ∘ g := asymptotics.is_equivalent.left_comp_log_of_tendsto_at_top' h (h.tendsto_at_top_iff.mp htop) -- to mathlib lemma asymptotics.is_o.congr_is_equivalent_left {u v w: ℝ → ℝ} {l: filter ℝ} (ho: is_o v w l) (h_equiv: u ~[l] v) : is_o u w l := begin convert is_o.add (is_o.trans h_equiv ho) ho, simp, end -- to mathlib lemma real.is_o_id_exp_at_top : is_o id real.exp at_top := begin refine (asymptotics.is_o_iff_tendsto $ λ (x : ℝ) hx, (x.exp_pos.ne hx.symm).elim).mpr _, convert real.tendsto_div_pow_mul_exp_add_at_top 1 0 1 zero_ne_one (le_refl _), ext, simp end -- to mathlib lemma real.is_o_log_id_at_top: is_o real.log id at_top := asymptotics.is_o.congr' (eventually_eq.refl _ _) ((eventually_gt_at_top 0).mono $ λ x hx, real.exp_log hx) (real.is_o_id_exp_at_top.comp_tendsto real.tendsto_log_at_top) lemma tendsto_log1_plus_x_under_x_at_top_nhds_0 : tendsto (λ (x : ℝ), real.log (1 + x) / x) at_top (𝓝 0) := have this : 1 + id ~[at_top] id := (is_equivalent.refl).add_is_o (asymptotics.is_o_one_iff_left.mpr tendsto_norm_at_top_at_top), (real.is_o_log_id_at_top.congr_is_equivalent_left $ this.left_comp_log_of_tendsto_at_top' tendsto_id).tendsto_0
so beautiful
Anatole Dedecker (Aug 18 2021 at 23:08):
Oh and I forgot some easy generalizations, wait a second
Ryan Lahfa (Aug 18 2021 at 23:08):
I +1 the condition on left_comp_log_of_tendsto_at_top
, it should be enough to say that f is eventually not approaching 1.
Ryan Lahfa (Aug 18 2021 at 23:09):
it should be cool to write down that log (1 + x) / x^n → 0
and log = o(x^n)
in fact for any n ≥ 1 I think (?)
Yaël Dillies (Aug 18 2021 at 23:17):
for any n
!
Ryan Lahfa (Aug 18 2021 at 23:24):
Yaël Dillies said:
for any
n
!
but when ?!
Anatole Dedecker (Aug 18 2021 at 23:24):
Ryan Lahfa said:
it should be cool to write down that
log (1 + x) / x^n → 0
andlog = o(x^n)
in fact for any n ≥ 1 I think (?)
Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.
Ryan Lahfa (Aug 18 2021 at 23:24):
Anatole Dedecker said:
Ryan Lahfa said:
it should be cool to write down that
log (1 + x) / x^n → 0
andlog = o(x^n)
in fact for any n ≥ 1 I think (?)Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.
The theorem for the limits already exist, but for reals > 0 do not I believe, so more generalization to do :>
Anatole Dedecker (Aug 18 2021 at 23:26):
I think Yaël might have thought that we are talking about ?
Anatole Dedecker (Aug 18 2021 at 23:29):
Ryan Lahfa said:
Anatole Dedecker said:
Ryan Lahfa said:
it should be cool to write down that
log (1 + x) / x^n → 0
andlog = o(x^n)
in fact for any n ≥ 1 I think (?)Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.
The theorem for the limits already exist, but for reals > 0 do not I believe, so more generalization to do :>
Which theorem are you thinking about ? (the one that already exists)
Ryan Lahfa (Aug 18 2021 at 23:30):
Anatole Dedecker said:
Ryan Lahfa said:
Anatole Dedecker said:
Ryan Lahfa said:
it should be cool to write down that
log (1 + x) / x^n → 0
andlog = o(x^n)
in fact for any n ≥ 1 I think (?)Yes, it should be pretty easy to generalize to naturals ≥ 1. It should also be possible to generalize to reals > 0, though it may be a bit harder.
The theorem for the limits already exist, but for reals > 0 do not I believe, so more generalization to do :>
Which theorem are you thinking about ? (the one that already exists)
docs#real.tendsto_pow_mul_exp_neg_at_top_nhds_0
Anatole Dedecker (Aug 18 2021 at 23:32):
Oh yeah the exp
one
Anatole Dedecker (Aug 18 2021 at 23:35):
Indeed I can't find it for rpow
Anatole Dedecker (Aug 18 2021 at 23:36):
Also, feel free to PR any part of my code if you want to take care of it.
Ryan Lahfa (Aug 18 2021 at 23:36):
It might be feasible to make it so that with would be the general theorem, so we could have the generalization over reals with limits of form
Ryan Lahfa (Aug 18 2021 at 23:37):
Anatole Dedecker said:
Also, feel free to PR any part of my code if you want to take care of it.
If you prefer to do it, feel free, in all cases, I will try to PR some parts of my project (Ostrowski theorems) so it will be an arduous path, if I come around your parts and no PR is opened, or you do not have time, I am okay with shepherding it and doing the required changes :)
Anatole Dedecker (Aug 18 2021 at 23:44):
Ryan Lahfa said:
Anatole Dedecker said:
Also, feel free to PR any part of my code if you want to take care of it.
If you prefer to do it, feel free, in all cases, I will try to PR some parts of my project (Ostrowski theorems) so it will be an arduous path, if I come around your parts and no PR is opened, or you do not have time, I am okay with shepherding it and doing the required changes :)
I can do it, but I have other PRs to work on, so it might wait a little. If you're okay with that then I'll take care of the PR.
Ryan Lahfa (Aug 18 2021 at 23:49):
Anatole Dedecker said:
Ryan Lahfa said:
Anatole Dedecker said:
Also, feel free to PR any part of my code if you want to take care of it.
If you prefer to do it, feel free, in all cases, I will try to PR some parts of my project (Ostrowski theorems) so it will be an arduous path, if I come around your parts and no PR is opened, or you do not have time, I am okay with shepherding it and doing the required changes :)
I can do it, but I have other PRs to work on, so it might wait a little. If you're okay with that then I'll take care of the PR.
Definitely not in a hurry, thanks!
Last updated: Dec 20 2023 at 11:08 UTC