Zulip Chat Archive

Stream: triage

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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