`BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor` (e : E) (l μ : ℕ) (x : E) : HasFDerivAt (radialFactor e l μ) (∑ m ∈ Finset.range ((l - μ) / 2 + 1), ((derivative^[μ] (lege

Proved

BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSolidHarmonic.

BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor (e : E) (l μ : ℕ) (x : E) : HasFDerivAt (radialFactor e l μ) (∑ m ∈ Finset.range ((l - μ) / 2 + 1), ((derivative^[μ] (legendre l)).coeff (l - μ - 2 * m)) • ((((l - μ - 2 * m : ℕ) : ℝ) * (⟪e, x⟫_ℝ) ^ (l - μ - 2 * m - 1) * (‖x‖ ^ 2) ^ m) • innerCLM E e + (2 * m * (⟪e, x⟫_ℝ) ^ (l - μ - 2 * m) * (‖x‖ ^ 2) ^ (m - 1)) • innerCLM E x)) x

Formalization note: Lean 4 identifier BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor.

Preamble

-- Generated from ChapterSolidHarmonic.lean — theorem BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor
import Definitions.Def_ChapterLaplacianProduct
import Definitions.Def_ChapterSolidHarmonicTools
import Mathlib
import Definitions.Def_ChapterSolidHarmonic
import Definitions.Def_ChapterLegendrePolynomial
import Definitions.Def_ChapterRadialLaplacian
open BookProof.ChapterLegendrePolynomial
open BookProof.ChapterRadialLaplacian
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]

Formal statement

theorem BookProof.ChapterSolidHarmonic.hasFDerivAt_radialFactor (e : E) (l μ : ℕ) (x : E) :
    HasFDerivAt (radialFactor e l μ)
      (∑ m ∈ Finset.range ((l - μ) / 2 + 1),
        ((derivative^[μ] (legendre l)).coeff (l - μ - 2 * m)) •
          ((((l - μ - 2 * m : ℕ) : ℝ) * (⟪e, x⟫_ℝ) ^ (l - μ - 2 * m - 1) * (‖x‖ ^ 2) ^ m)
              • innerCLM E e
            + (2 * m * (⟪e, x⟫_ℝ) ^ (l - μ - 2 * m) * (‖x‖ ^ 2) ^ (m - 1)) • innerCLM E x)) x := by sorry

View graph