rpow_nat_cast for non-integers exponents?

Stream: general

[Ryan Lahfa]

I'm trying to formalize the following fact $\lim_n C^{1/n} = 1$ for $C > 0$ a real and I have this little certainly ineffective proof:

import analysis.special_functions.pow


lemma tendsto_root_at_top_nhds_1_of_pos {C: ℝ} (c_pos: C > 0):
  filter.tendsto (λ (n: ℕ), C^(1 / n)) filter.at_top (nhds 1) :=
begin
  have h_exp_form: (λ (n: ℕ), C^(1/n)) = (λ (n: ℕ), real.exp((real.log C) / n)),
  {
    ext,
    rw ← real.rpow_nat_cast,
    -- why is this even possible?
    rw real.rpow_def_of_pos c_pos (↑(1 / x)),
    sorry,
  },
  {
    rw h_exp_form,
    apply filter.tendsto.comp,
    apply real.tendsto_exp_nhds_0_nhds_1,
    apply tendsto_const_div_at_top_nhds_0_nat,
  }
end

I am really wondering why I can "cast" 1 / n while it's not really an integer exponent? Also, is there a nice way to move forward with the cast? I tried multiple approaches but unsure of what would be canonical at this step.

I understand well that the issue here is that I'm mixing multiple instances of has_pow but I feel like it should be okay?

[Heather Macbeth]

Do you want to follow this approach in particular, or are you open to other approaches? If you're open to other approaches, why don't you consider the composition of the limits $\lim_{x\to 0}C^x=1$ and $\lim_{n\to\infty}\frac{1}{n}=0$?

[Alex J. Best]

If you're in Vscode you can hover over the 1/n to see that it is the natural number division (hence 0 for n > 1) rather than what you want.

[Ryan Lahfa]

Heather Macbeth said:

Do you want to follow this approach in particular, or are you open to other approaches? If you're open to other approaches, why don't you consider the composition of the limits $\lim_{x\to 0}C^x=1$ and $\lim_{n\to\infty}\frac{1}{n}=0$?

I'm open to other approaches indeed, I am just looking to learn more of getting out of tricky cast situations as I expect to run into many of them in a close future

[Alex J. Best]

lemma tendsto_root_at_top_nhds_1_of_pos {C: ℝ} (c_pos: C > 0):
  filter.tendsto (λ (n: ℕ), C^((1 :ℝ)/ n)) filter.at_top (nhds 1) :=
begin
  have h_exp_form: (λ (n: ℕ), C^((1:ℝ)/n)) = (λ (n: ℕ), real.exp((real.log C) / n)),
  {
    ext,
    simp,
    rw div_eq_mul_inv,
    rw real.exp_mul,
    rw real.exp_log c_pos,
  },
  {
    rw h_exp_form,
    apply filter.tendsto.comp,
    apply real.tendsto_exp_nhds_0_nhds_1,
    apply tendsto_const_div_at_top_nhds_0_nat,
  }
end

[Ryan Lahfa]

Alex J. Best said:

If you're in Vscode you can hover over the 1/n to see that it is the natural number division (hence 0 for n > 1) rather than what you want.

Indeed

[Ryan Lahfa]

lemma tendsto_root_at_top_nhds_1_of_pos {C: ℝ} (c_pos: C > 0):
  filter.tendsto (λ (n: ℕ), C^((1: ℝ) / n)) filter.at_top (nhds 1) :=
begin
  have h_exp_form: (λ (n: ℕ), C^((1: ℝ)/n)) = (λ (n: ℕ), real.exp((real.log C) / n)),
  {
    ext,
    rw real.rpow_def_of_pos c_pos,
    congr' 1,
    rw ← mul_div_assoc,
    simp,
  },
  {
    rw h_exp_form,
    apply filter.tendsto.comp,
    apply real.tendsto_exp_nhds_0_nhds_1,
    apply tendsto_const_div_at_top_nhds_0_nat,
  }
end

seems to close the goal, thanks @Alex J. Best and @Heather Macbeth !

[Ryan Lahfa]

Ah thanks for the alternative proof !