Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,039 to 1,044 of 2,569 results.
f₂_add_f₄_eq_f₃
Mathematical statement
The error terms satisfy f₂ + f₄ = f₃ (from Jacobi identity)
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₂_eq_zero
Mathematical statement
From g = 0 and h = 0, deduce f₂ = 0. Proof: From g = 0 we get a relation between f₂ and f₄. Combined with h = 0, we show f₄² · (3 · H_sum_sq) = 0. Since H_sum_sq → 1 ≠ 0, we get f₄ = 0, then f₂ = 0 follows from h = f₂² = 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₂_S_action
Mathematical statement
f₂ transforms under S as f₂|S = -f₄. Proof outline using serre_D_slash_equivariant: 1. (serre_D 2 H₂)|[4]S = serre_D 2 (H₂|[2]S) = serre_D 2 (-H₄) = -serre_D 2 H₄ 2. (H₂(H₂ + 2H₄))|[4]S = (-H₄)((-H₄) + 2(-H₂)) = H₄(H₄ + 2H₂) 3. f₂|[4]S = -serre_D 2 H₄ - (1/6)H₄(H₄ + 2H₂) = -f₄ Key lemmas used: - serre_D_slash_equivariant: (serre_D k F)|[k+2]γ = serre_D k...
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₂_T_action
Mathematical statement
f₂ transforms under T as f₂|T = -f₂. Proof outline: 1. (serre_D 2 H₂)|[4]T = serre_D 2 (H₂|[2]T) = serre_D 2 (-H₂) = -serre_D 2 H₂ 2. (H₂(H₂ + 2H₄))|[4]T = (-H₂)((-H₂) + 2H₃) Using Jacobi H₃ = H₂ + H₄: -H₂ + 2H₃ = -H₂ + 2(H₂ + H₄) = H₂ + 2H₄ So: (H₂(H₂ + 2H₄))|[4]T = (-H₂)(H₂ + 2H₄) 3. f₂|[4]T = -serre_D 2 H₂ - (1/6)(-H₂)(H₂ + 2H₄) = -serre_D 2 H₂ + (1/6)...
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₂_tendsto_atImInfty
Mathematical statement
f₂ tends to 0 at infinity. Proof: f₂ = serre_D 2 H₂ - (1/6)H₂(H₂ + 2H₄) Since H₂ → 0, both serre_D 2 H₂ → 0 and H₂(H₂ + 2H₄) → 0, so f₂ → 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₄_S_action
Mathematical statement
f₄ transforms under S as f₄|S = -f₂. Proof outline (symmetric to f₂_S_action): 1. (serre_D 2 H₄)|[4]S = serre_D 2 (H₄|[2]S) = serre_D 2 (-H₂) = -serre_D 2 H₂ 2. (H₄(2H₂ + H₄))|[4]S = (-H₂)(2(-H₄) + (-H₂)) = H₂(H₂ + 2H₄) 3. f₄|[4]S = -serre_D 2 H₂ + (1/6)H₂(H₂ + 2H₄) = -f₂
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.