Beginner Lean Question

Stream: PrimeNumberTheorem+

[milomg]

I've been working on a proof of tendsto_Realpow_atTop_nhds_0_of_norm_gt_1 that uses Tendsto.comp, but it ended up being quite a bit less clean than I expected. Im curious what would be some strategies and/or style tips to improve this proof?

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.Calculus.ContDiff.Basic

open Complex Topology Filter Real

lemma tendsto_Realpow_atTop_nhds_0_of_norm_lt_1 {x : ℝ}  (xpos : 0 < x) (x_lt_one : x < 1) (C : ℝ) :
  Tendsto (fun (σ : ℝ) => x ^ σ * C) atTop (𝓝 0) := by
  sorry

lemma tendsto_Realpow_atTop_nhds_0_of_norm_gt_1 {x : ℝ} {C : ℝ} (x_gt_one : 1 < x) (Cpos : C > 0) :
    Tendsto (fun (σ : ℝ) => x ^ σ * C) atBot (𝓝 0) := by
  have h: Tendsto (fun (σ : ℝ) => x ^ (-σ) * C) atTop (𝓝 0) := by
    have := (lt_trans zero_lt_one x_gt_one)
    conv in (x ^ (-_) * C) =>
      rw [rpow_neg (le_of_lt this), ← inv_rpow (le_of_lt this)]
    exact tendsto_Realpow_atTop_nhds_0_of_norm_lt_1 (inv_pos.mpr this) (inv_lt_one x_gt_one) C
  have := Tendsto.comp h tendsto_neg_atBot_atTop
  conv at this =>
    congr
    ext
    rw [@Function.comp_apply, neg_neg]
  exact this

Update: my proof now looks like this

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
import Mathlib.Analysis.Calculus.ContDiff.Basic

open Complex Topology Filter Real

lemma tendsto_rpow_atTop_nhds_zero_of_norm_lt_one {x : ℝ}  (xpos : 0 < x) (x_lt_one : x < 1) (C : ℝ) :
  Tendsto (fun (σ : ℝ) => x ^ σ * C) atTop (𝓝 0) := by
  have := Tendsto.mul_const C (tendsto_rpow_atTop_of_base_lt_one x (by linarith) x_lt_one)
  simp only [rpow_eq_pow, zero_mul] at this
  exact this

lemma tendsto_rpow_atTop_nhds_zero_of_norm_gt_one {x : ℝ} (x_gt_one : 1 < x) (C : ℝ) :
    Tendsto (fun (σ : ℝ) => x ^ σ * C) atBot (𝓝 0) := by
  have : 0 < x := zero_lt_one.trans x_gt_one
  convert (tendsto_rpow_atTop_nhds_zero_of_norm_lt_one (inv_pos.mpr this) (inv_lt_one x_gt_one) C).comp tendsto_neg_atBot_atTop using 1
  ext; simp only [this.le, inv_rpow, Function.comp_apply, rpow_neg, inv_inv]

[Bolton Bailey]

I usually try to avoid conv blocks, in this case it looks like you can replace the conv with simp only [Function.comp_def, neg_neg] at this .

[milomg]

Aha, thank you!

[Bolton Bailey]

I guess my first thought when trying to approach this proof would be to ask, is there a way I can simplify away the * C at the beginning. docs#Filter.Tendsto.mul_const looks like it could be helpful there.

[Bolton Bailey]

Or maybe docs#Filter.tendsto_mul_const_atBot_iff

[Yury G. Kudryashov]

Not atBot, it's about functions that tend to -∞.

[Ruben Van de Velde]

Perhaps:

lemma tendsto_Realpow_atTop_nhds_0_of_norm_gt_1' {x : ℝ} {C : ℝ} (x_gt_one : 1 < x) (Cpos : C > 0) :
    Tendsto (fun (σ : ℝ) => x ^ σ * C) atBot (𝓝 0) := by
  have : 0 < x := zero_lt_one.trans x_gt_one
  convert (tendsto_Realpow_atTop_nhds_0_of_norm_lt_1 (inv_pos.mpr this) (inv_lt_one x_gt_one) C).comp tendsto_neg_atBot_atTop using 1
  ext; simp [this.le, inv_rpow, rpow_neg]

[Yury G. Kudryashov]

It's by simpa only [zero_mul] using (tendsto_rpow_atBot_of_base_gt_one x_gt_one).mul tendsto_const_nhds (untested)

[Yury G. Kudryashov]

docs#tendsto_rpow_atBot_of_base_gt_one

[Yury G. Kudryashov]

It would be nice if someone makes a PR reformulating this and nearby lemmas in terms of ^ instead of Real.rpow.

[Michael Stoll]

(As an aside, the name should use "zero" and "one" in place of "0" and "1".)

[Ruben Van de Velde]

Also rpow rather than Realpow

[Ruben Van de Velde]

Yury G. Kudryashov said:

It would be nice if someone makes a PR reformulating this and nearby lemmas in terms of ^ instead of Real.rpow.

(These come out of #6140 from @Frédéric Dupuis)

[Yury G. Kudryashov]

BTW, you don't need C > 0 for your lemma.

[Bolton Bailey]

Do we have an iff version of docs#Filter.Tendsto.mul_const for nhds? Something that tells us we can divide off the c?

[Yury G. Kudryashov]

The iff version would need C ≠ 0

[milomg]

Maybe something like docs#tendsto_const_smul_iff

[Yury G. Kudryashov]

It would be nice to have a tactic tendsto that goes from inside out and tracks the best filter we have.

[Alex Kontorovich]

Sorry, you're working on part 6, tendsto_Realpow_atTop_nhds_0_of_norm_gt_1? I already marked it as finished (thanks to a hint by @Yury G. Kudryashov)...

[milomg]

Oops, does that mean I picked something off of the blueprint that may have already been completed? (is it possible Yury's hint was for tendsto_Realpow_atTop_nhds_0_of_norm_lt_1?).

If it is already completed, I'm happy to close my PR

[Alex Kontorovich]

Oh I see, sorry; you're doing gt, not lt. Thanks!

[Alex Kontorovich]

You're ahead of the game, I hadn't added that to the "Outstanding Tasks" list yet! :)

[milomg]

I attempted DeltaSpikeMass and ended up relying on conv again (simp only loops forever because of mul_comm). Are there tactics that exist or we could create that would make simp/ring work well on reals+subtypes inside integrals?

import Mathlib.Analysis.Complex.CauchyIntegral
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.MeasureTheory.Integral.IntegralEqImproper

open Complex Topology Filter Real

noncomputable def DeltaSpike (Ψ : ℝ → ℝ) (ε : ℝ) : ℝ → ℝ :=
  fun x => Ψ (x ^ (1 / ε)) / ε

lemma DeltaSpikeMass {Ψ : ℝ → ℝ} (mass_one: ∫ x in Set.Ioi 0, Ψ x / x = 1) (ε : ℝ) (εpos : 0 < ε) :
    ∫ x in Set.Ioi 0, ((DeltaSpike Ψ ε) x) / x = 1 := by
  unfold DeltaSpike
  have x1ε_nz := fun (x: (@Set.Elem ℝ (Set.Ioi 0))) =>
    ne_of_gt (Real.rpow_pos_of_pos x.property.out (1 / ε))
  have :
    ∫ (x : ℝ) in Set.Ioi 0, Ψ (x ^ (1 / ε)) / ε / x =
    ∫ (x : ℝ) in Set.Ioi 0, (|1/ε| * x ^ (1 / ε - 1)) • ((fun z => (Ψ z) / z)  (x ^ (1 / ε))) := by
    simp only [smul_eq_mul, ← (MeasureTheory.integral_subtype (measurableSet_Ioi (a := (0 : ℝ))))]
    rw [abs_of_pos (one_div_pos.mpr εpos)]
    conv =>
      rhs ; congr ; rfl
      intro x
      rw [mul_comm, mul_comm (1/ε) _, ← mul_assoc,
      rpow_sub x.property.out, rpow_one, ← mul_div_assoc,
      ← mul_div_assoc, div_mul_cancel _ (x1ε_nz _), mul_one, div_right_comm]
  rw [this, MeasureTheory.integral_comp_rpow_Ioi (fun z => (Ψ z) / z), ← mass_one]
  simp only [ne_eq, div_eq_zero_iff, one_ne_zero, εpos.ne', or_self, not_false_eq_true]

[Terence Tao]

I find docs#MeasureTheory.set_integral_congr (and similar tools) to suffice for manipulating integrands, particularly when done inside a calc block.