10 million heartbeats (!4#3242)

Stream: mathlib4

[Jeremy Tan]

In fixing !4#3242 I think I've found a new record for most heartbeats needed to show definitional equality: 10 MILLION. 1 million doesn't work.

set_option maxHeartbeats 10000000 in -- XXX XXX XXX XXX XXX XXX XXX XXX XXX XXX TODO
theorem tendsto_pow_atTop_nhds_0_of_lt_1 {𝕜 : Type _} [LinearOrderedField 𝕜] [Archimedean 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
    Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) := by
  cases' h₁.eq_or_lt with h h
  · exact (tendsto_add_atTop_iff_nat 1).mp <| by simp only [_root_.pow_succ, ← h, zero_mul,
      tendsto_const_nhds_iff]
  · have : Tendsto (fun n => (r⁻¹ ^ n)⁻¹) atTop (𝓝 0) :=
      tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt <| one_lt_inv h h₂)
    exact this.congr fun n => by simp

[Jeremy Tan]

Surely @Matthew Ballard can help with this (and perhaps the rest of the file)?

[Matthew Ballard]

/me is currently depreciating an hvac system for taxes

[Jeremy Tan]

/me is testing that feature from Pokémon Showdown

[MonadMaverick]

theorem tendsto_pow_atTop_nhds_0_of_lt_1 {𝕜 : Type _} [LinearOrderedField 𝕜] [Archimedean 𝕜]
    [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
    Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) :=
  h₁.eq_or_lt.elim
    (fun hr => (tendsto_add_atTop_iff_nat 1).mp <| by simp [_root_.pow_succ, ← hr, tendsto_const_nhds])
    (fun hr =>
      have := one_lt_inv hr h₂ |> tendsto_pow_atTop_atTop_of_one_lt
      (tendsto_inv_atTop_zero.comp this).congr fun n => by simp)
#align tendsto_pow_at_top_nhds_0_of_lt_1 tendsto_pow_atTop_nhds_0_of_lt_1

This seems to be fine.

[MonadMaverick]

All fixed. Basic.lean
I'll push my commits tonight

[Jeremy Tan]

You have not solved the very last error

[Jeremy Tan]

theorem exists_pos_tsum_mul_lt_of_countable {ε : ℝ≥0∞} (hε : ε ≠ 0) {ι} [Countable ι] (w : ι → ℝ≥0∞)
    (hw : ∀ i, w i ≠ ∞) : ∃ δ : ι → ℝ≥0, (∀ i, 0 < δ i) ∧ (∑' i, (w i * δ i : ℝ≥0∞)) < ε := by
  lift w to ι → ℝ≥0 using hw
  rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩
  have : ∀ i, 0 < max 1 (w i) := fun i => zero_lt_one.trans_le (le_max_left _ _)
  refine' ⟨fun i => δ' i / max 1 (w i), fun i => div_pos (Hpos _) (this i), _⟩
  refine' lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i => _) Hsum
  rw [coe_div (this i).ne']
  refine' mul_le_of_le_div' (mul_le_mul_left' (ENNReal.inv_le_inv.2 _) _)
  exact coe_le_coe.2 (le_max_right _ _

[MonadMaverick]

really? somebody else also pushed. I'll have a look.

[Jeremy Tan]

Though to give you credit, I've incorporated some of your fixes in there

[MonadMaverick]

I think Komyyy <pol_tta@outlook.jp> pushed another fix independently.

[MonadMaverick]

I've pushed my version as tmp.lean.

It's strange that compiler doesn't complain about exists_pos_tsum_mul_lt_of_countable in my version.

[MonadMaverick]

@Pol'tta / Kô Miyahara

[MonadMaverick]

I've fixed the last error. @Jeremy Tan

[Jeremy Tan]

I've traced the problem to the inclusion of algebraMap; adding open algebraMap causes the error, and without it that last error disappears

[Jeremy Tan]

@Yaël Dillies why?

[MonadMaverick]

looks like the ugly fix works

ugly one:

theorem tendsto_coe_nat_div_add_atTop {𝕜 : Type _} [DivisionRing 𝕜] [TopologicalSpace 𝕜]
    [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜] [TopologicalDivisionRing 𝕜] (x : 𝕜) :
    Tendsto (fun n : ℕ => (n : 𝕜) / (n + x)) atTop (𝓝 1) := by
  refine' Tendsto.congr' ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => _)) _
  · exact fun n : ℕ => 1 / (1 + x / n)
  · field_simp [Nat.cast_ne_zero.mpr hn]
  · have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * (0 : 𝕜))) := by
      rw [MulZeroClass.mul_zero, add_zero, div_one]
    rw [this]
    refine' tendsto_const_nhds.div (tendsto_const_nhds.add _) (by simp)
    simp_rw [div_eq_mul_inv]
    refine' tendsto_const_nhds.mul _
    have : (fun n : ℕ => (n : 𝕜)⁻¹) = fun n : ℕ => (n : 𝕜)⁻¹ := by
      ext1 n
      rw [← map_natCast (algebraMap ℝ 𝕜) n, ← map_inv₀ (algebraMap ℝ 𝕜)]
    rw [this]
    have := ((continuous_algebraMap ℝ 𝕜).tendsto _).comp tendsto_inverse_atTop_nhds_0_nat
    simp at this
    refine' Iff.mpr tendsto_atTop' _
    rw [tendsto_atTop'] at this
    intro s hs
    specialize this s hs
    choose a ha using this
    exists a
    intro b hb
    specialize ha b hb
    simp [Set.mem_def] at ha
    exact ha
#align tendsto_coe_nat_div_add_at_top tendsto_coe_nat_div_add_atTop

theorem tendsto_coe_nat_div_add_atTop {𝕜 : Type _} [DivisionRing 𝕜] [TopologicalSpace 𝕜]
    [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜] [TopologicalDivisionRing 𝕜] (x : 𝕜) :
    Tendsto (fun n : ℕ => (n : 𝕜) / (n + x)) atTop (𝓝 1) := by
  refine' Tendsto.congr' ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => _)) _
  · exact fun n : ℕ => 1 / (1 + x / n)
  · field_simp [Nat.cast_ne_zero.mpr hn]
  · have : 𝓝 (1 : 𝕜) = 𝓝 (1 / (1 + x * ↑(0 : ℝ))) := by
      rw [algebraMap.coe_zero, MulZeroClass.mul_zero, add_zero, div_one]
    rw [this]
    refine' tendsto_const_nhds.div (tendsto_const_nhds.add _) (by simp)
    simp_rw [div_eq_mul_inv]
    refine' tendsto_const_nhds.mul _
    have : (fun n : ℕ => (n : 𝕜)⁻¹) = fun n : ℕ => ↑(n⁻¹ : ℝ) := by
      ext1 n
      rw [← map_natCast (algebraMap ℝ 𝕜) n, ← map_inv₀ (algebraMap ℝ 𝕜)]
      rfl
    rw [this]
    exact ((continuous_algebraMap ℝ 𝕜).tendsto _).comp tendsto_inverse_atTop_nhds_0_nat
#align tendsto_coe_nat_div_add_at_top tendsto_coe_nat_div_add_atTop

[MonadMaverick]

must be some function name collision shenanigans

[Jeremy Tan]

There, all done!