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

Stream: triage

[Random Issue Bot]

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]

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]

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]

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

[Yakov Pechersky]

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

[Random Issue Bot]

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, merge-conflict

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

[Random Issue Bot]

Today I chose PR 5521 for discussion!

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

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