## Stream: triage

### Topic: PR #5521: feat(analysis/calculus/deriv): let simp compute...

#### Random Issue Bot (Mar 19 2021 at 14:21):

Today I chose PR 5521 for discussion!

feat(analysis/calculus/deriv): let simp compute deriv of x⁻¹
Created by @None (@hrmacbeth) on 2020-12-29
Labels: awaiting-author

Is this PR still relevant? Any recent updates? Anyone making progress?

#### Heather Macbeth (Mar 19 2021 at 18:41):

There is nothing really wrong with this PR. It just has a long, ugly proof which should be golfed before it joins mathlib. I'll post it here in case anyone is inspired.

#### Heather Macbeth (Mar 19 2021 at 18:45):

import analysis.specific_limits

open_locale topological_space
open filter

@[simp] lemma normed_field.continuous_at_fpow_iff
{𝕜 : Type*} [nondiscrete_normed_field 𝕜] {m : ℤ} {x : 𝕜} :
continuous_at (λx:𝕜, x^m) x ↔ (x ≠ 0 ∨ 0 ≤ m) :=
begin
have : ∀ m : ℤ, 0 < m → continuous_at (λx, x^m) x,
{ assume m hm,
lift m to ℕ using (le_of_lt hm),
exact (continuous_pow m).continuous_at },
rcases lt_trichotomy m 0 with hm|hm|hm,
{ have : ¬ (0 ≤ m) := not_le.mpr hm,
simp only [this, or_false, ne.def],
lift -m to ℕ using le_of_lt (neg_pos.mpr hm) with k hk,
have hk' : m = -↑k := eq_neg_of_eq_neg hk,
suffices : continuous_at (λ x, (x ^ k)⁻¹) x ↔ x ≠ 0,
{ convert this,
ext y,
simp [hk'] },
split,
{ rintros h rfl,
suffices h' : tendsto (λ x : 𝕜, ∥(x ^ k)⁻¹∥) (𝓝[{0}ᶜ] 0) at_top,
{ haveI := normed_field.punctured_nhds_ne_bot (0:𝕜),
apply not_tendsto_nhds_of_tendsto_at_top h' _,
exact (continuous_norm.continuous_at.comp h).continuous_within_at.tendsto },
refine normed_field.tendsto_norm_inverse_nhds_within_0_at_top.comp _,
change tendsto _ _ (_ ⊓ _),
rw filter.tendsto_inf,
split,
{ apply tendsto_nhds_within_of_tendsto_nhds,
convert (continuous_pow k).continuous_at.tendsto,
{ refine (zero_pow _).symm,
rw hk' at hm,
exact_mod_cast neg_lt_zero.mp hm },
apply_instance },
simp only [tendsto_principal],
refine ⟨set.univ, univ_mem_sets, {(0:𝕜)}ᶜ, by simp, _⟩,
rw set.univ_inter,
exact λ _, mt pow_eq_zero },
{ intros h,
refine continuous_at.comp _ (continuous_pow k).continuous_at,
refine continuous_at_inv' _,
exact pow_ne_zero k h } },
{ simp [hm, fpow_zero, int.cast_zero, zero_mul, continuous_at_const, rfl.ge] },
{ simp [this m hm, le_of_lt hm] }
end


#### Yakov Pechersky (Mar 19 2021 at 19:08):

Does this get any better with my #6757 proving more things about fpow and having that be available via norm_fpow?

#### Yakov Pechersky (Mar 19 2021 at 19:09):

Or is that just covered by your { simp [hm, fpow_zero, int.cast_zero, zero_mul, continuous_at_const, rfl.ge] }?

Last updated: May 09 2021 at 15:11 UTC