Zulip Chat Archive

Stream: new members

Topic: normed and discrete_linear_ordered field


Anatole Dedecker (Oct 26 2020 at 10:07):

Hello, I'm having some troubles working with a field that is both a normed_field and a discrete_linear_ordered_field : in the following mwe, the last line yields an error, which I interpret as "Lean doesn't know which field instance to use". What should I do to avoid this ?

import analysis.calculus.deriv

open filter asymptotics

open_locale topological_space

lemma tendsto_pow_div_pow {α : Type*} [normed_field α] [discrete_linear_ordered_field α]
  {p q : } (hpq : p < q) : is_o (λ (x : α), x^p) (λ x, x^q) at_top :=
begin
  rw is_o_iff_tendsto sorry,
  suffices h : tendsto (λ (x : α), x ^ ((p : ) - q)) at_top (𝓝 0),
  { refine (tendsto_congr' ((eventually_gt_at_top (0 : α)).mono (λ x hx, _))).mp h,
    simp [fpow_sub hx.ne.symm] },
  rw  neg_sub,
  rw  int.coe_nat_sub hpq.le,
  have : 1  q - p := nat.sub_pos_of_lt hpq,
  exact @tendsto_pow_neg_at_top α _ _ (by apply_instance) _ this,
end

Kenny Lau (Oct 26 2020 at 11:12):

this is called a diamond

Kenny Lau (Oct 26 2020 at 11:13):

if you can't remove the diamond from the assumptions, create a new typeclass that merges the two

Johan Commelin (Oct 26 2020 at 12:02):

In other words, you'll need to define linear_ordered_normed_field

Patrick Massot (Oct 26 2020 at 13:23):

You can also do everything with real numbers and leave a TODO note saying that once someone will have cleaned the order hierarchy then this will be available for generalization.


Last updated: Dec 20 2023 at 11:08 UTC