`BookProof.ChapterSolidHarmonic.norm_spherePt` {r : ℝ} (hr : 0 ≤ r) (θ φ : ℝ) : ‖spherePt u v e r θ φ‖ = r
DisprovedBookProof.ChapterSolidHarmonic.norm_spherePtProve the following Lean 4 theorem from ChapterSolidHarmonic.
BookProof.ChapterSolidHarmonic.norm_spherePt {r : ℝ} (hr : 0 ≤ r) (θ φ : ℝ) : ‖spherePt u v e r θ φ‖ = r
Formalization note: Lean 4 identifier BookProof.ChapterSolidHarmonic.norm_spherePt.
Retired 2026-10-30 — superseded by a corrected statement, not withdrawn. The exported target lost the normality of the frame: hu hv he were section variables that do not occur in the type, so the target asserted for arbitrary vectors, which fails as soon as they are not of norm one.
Where the fix lives. In the source of record the hypothesis is an explicit binder of the declaration, so a re-export cannot lose it:
BookProof.ChapterSolidHarmonic.norm_spherePt_frames_explicitintimepiece/BookProof/HarmonicAnalysis/ChapterSolidHarmonic.lean(Lean 4.28 tree),BookProof.ChapterSolidHarmonic.norm_spherePt_frames_explicitintimepiece331/BookProof/ChapterSolidHarmonic.lean(Lean 4.33.1 tree).
It is published on the platform as BookProof.ChapterSolidHarmonic.norm_spherePt_frames_explicit. This record stays readable and importable for anything already citing it; its proof status is unchanged.
-- Generated from ChapterSolidHarmonic.lean — theorem BookProof.ChapterSolidHarmonic.norm_spherePt
import Definitions.Def_ChapterRadialLaplacian
import Definitions.Def_ChapterLaplacianProduct
import Definitions.Def_ChapterSolidHarmonicTools
import Definitions.Def_ChapterLegendrePolynomial
import Mathlib
import Definitions.Def_ChapterSolidHarmonic
open BookProof.ChapterSolidHarmonic
open Laplacian InnerProductSpace Polynomial
open BookProof.ChapterRadialLaplacian BookProof.ChapterLaplacianProduct
open BookProof.ChapterSolidHarmonicTools BookProof.ChapterLegendrePolynomial
open scoped RealInnerProductSpace
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
variable {u v e : E} (hu : ‖u‖ = 1) (hv : ‖v‖ = 1) (he : ‖e‖ = 1)
(huv : ⟪u, v⟫_ℝ = 0) (hue : ⟪u, e⟫_ℝ = 0) (hve : ⟪v, e⟫_ℝ = 0)theorem BookProof.ChapterSolidHarmonic.norm_spherePt {r : ℝ} (hr : 0 ≤ r) (θ φ : ℝ) : ‖spherePt u v e r θ φ‖ = r := by sorry