F₄ tendsto at Im Infty
f₄_tendsto_atImInfty
Plain-language statement
f₄ tends to 0 at infinity. Proof: f₄ = serre_D 2 H₄ + (1/6)H₄(2H₂ + H₄) serre_D 2 H₄ = D H₄ - (1/6)E₂ H₄ → 0 - (1/6)11 = -1/6 (since H₄ → 1, E₂ → 1) H₄(2H₂ + H₄) → 1*(0 + 1) = 1 So f₄ → -1/6 + (1/6)*1 = 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.