Runtime Question of `tprod_sigma'`

Stream: mathlib4

[Fengyang Wang]

/-
# MWE: `rw [hsigma.tsum_sigma' h1]` causes heartbeat timeout

When using `Summable.tsum_sigma'` inside `rw`, Lean times out.
Workaround: compute result via `have` first, then use `▸` substitution.
-/

import Mathlib.Topology.Algebra.InfiniteSum.Basic
import Mathlib.Analysis.Normed.Group.InfiniteSum
import Mathlib.Analysis.Normed.Lp.lpSpace

open scoped ENNReal

variable {M : Type*} {R : Type*}

set_option maxHeartbeats 10000

/-- Multiplication map for fiber partition. -/
def mulMap [Mul M] : M × M → M := Function.uncurry (· * ·)

/-- Fiber over x under multiplication. -/
def mulFiber [Mul M] (x : M) : Set (M × M) := mulMap ⁻¹' {x}

example [Monoid M] [NormedRing R] (f g : lp (fun _ : M => R) 1)
    (hprod : Summable fun ab : M × M => ‖f ab.1‖ * ‖g ab.2‖)
    (hsigma : Summable fun p : Σ x, mulFiber x => ‖f p.2.1.1‖ * ‖g p.2.1.2‖)
    (h1 : ∀ m, Summable fun ab : mulFiber m => ‖(f : M → R) ab.1.1‖ * ‖g ab.1.2‖) :
    ∑' (p : Σ x, mulFiber x), ‖f p.2.1.1‖ * ‖g p.2.1.2‖ =
    ∑' x, ∑' ab : mulFiber x, ‖f ab.1.1‖ * ‖g ab.1.2‖ := by
  -- This works: compute result first
  have h2 : ∑' (p : Σ x, mulFiber x), ‖f p.2.1.1‖ * ‖g p.2.1.2‖ =
      ∑' x, ∑' ab : mulFiber x, ‖f ab.1.1‖ * ‖g ab.1.2‖ := hsigma.tsum_sigma' h1
  exact h2

example [Monoid M] [NormedRing R] (f g : lp (fun _ : M => R) 1)
    (hprod : Summable fun ab : M × M => ‖f ab.1‖ * ‖g ab.2‖)
    (hsigma : Summable fun p : Σ x, mulFiber x => ‖f p.2.1.1‖ * ‖g p.2.1.2‖)
    (h1 : ∀ m, Summable fun ab : mulFiber m => ‖(f : M → R) ab.1.1‖ * ‖g ab.1.2‖) :
    ∑' x, ∑' ab : mulFiber x, ‖f ab.1.1‖ * ‖g ab.1.2‖ =
    ∑' (p : Σ x, mulFiber x), ‖f p.2.1.1‖ * ‖g p.2.1.2‖ := by
  -- TIMEOUT: using rw directly causes heartbeat exceeded
  rw [hsigma.tsum_sigma' h1]
  -- (deterministic) timeout at `whnf`, maximum number of heartbeats (10000) has been reached

set_option maxHeartbeats 200000
example [Monoid M] [NormedRing R] (f g : lp (fun _ : M => R) 1)
    (hprod : Summable fun ab : M × M => ‖f ab.1‖ * ‖g ab.2‖)
    (hsigma : Summable fun p : Σ x, mulFiber x => ‖f p.2.1.1‖ * ‖g p.2.1.2‖)
    (h1 : ∀ m, Summable fun ab : mulFiber m => ‖(f : M → R) ab.1.1‖ * ‖g ab.1.2‖) :
    ∑' x, ∑' ab : mulFiber x, ‖f ab.1.1‖ * ‖g ab.1.2‖ =
    ∑' (p : Σ x, mulFiber x), ‖f p.2.1.1‖ * ‖g p.2.1.2‖ := by
  rw [hsigma.tsum_sigma' h1]
  -- Now this works with increased heartbeat limit

/-
###### Question ######

Why does `rw [hsigma.tsum_sigma' h1]` timeout, while computing `have h2 := hsigma.tsum_sigma' h1`
and then using `exact h2` (or `▸` substitution) works fine?

Is this a known issue with `rw` and dependent types / sigma types?

## Workaround

Instead of:
rw [hsigma.tsum_sigma' h1]

Use:
have h2 := hsigma.tsum_sigma' h1
exact h2.symm  -- or use ▸ for substitution
-/

tprod_sigma'

[Kevin Buzzard]

Switch the profiler on and see what's going on

[Fengyang Wang]

Kevin Buzzard said:

Switch the profiler on and see what's going on

I'm seeing something like

[0.399964] 💥️ Filter.map (fun s => ∑ b_1 ∈ s, (fun c => ?m.170 ⟨b, c⟩) b_1)
                                          (SummationFilter.unconditional (?m.169 b)).filter ≤
                                        nhds
                                          a =?= Filter.map
                                          (fun s => ∑ b_1 ∈ s, (fun ab => ‖↑f (↑ab).1‖ * ‖↑g (↑ab).2‖) b_1)
                                          (SummationFilter.unconditional ↑(mulFiber b)).filter ≤
                                        nhds a ▼
     [delta] [0.354647] ❌️ Filter.map (fun s => ∑ b_1 ∈ s, (fun c => ?m.170 ⟨b, c⟩) b_1)
                                            (SummationFilter.unconditional (?m.169 b)).filter ≤
                                          nhds
                                            a =?= Filter.map
                                            (fun s => ∑ b_1 ∈ s, (fun ab => ‖↑f (↑ab).1‖ * ‖↑g (↑ab).2‖) b_1)
                                            (SummationFilter.unconditional ↑(mulFiber b)).filter ≤
                                          nhds a ▼

[Aaron Liu]

does it run faster if you reverse the direction of the equality in the goal

[Fengyang Wang]

Aaron Liu said:

does it run faster if you reverse the direction of the equality in the goal

Haven't tried this, but I found a general workaround for something that is supposed to be right, but times out. Use a protected theorem to wrap the typeclass signature, then Lean infers a lot faster.

See the update in my PR

[Fengyang Wang]

@Aaron Liu Now I should have figured out the root of this problem.
Lastest update posted here

[Fengyang Wang]

@Kevin Buzzard I was able to figure out the cause with the help of the profiler, thanks!