def DistributionalKernels.multiIndexSize {n : ℕ} (γ : Fin n → ℕ) : ℕ

The size |γ| = ∑ γ i of a multi-index γ : Fin n → ℕ.

def DistributionalKernels.multiIndexLeqFinset {n : ℕ} (γ : Fin n → ℕ) : Finset (Fin n → ℕ)

The finite set of multi-indices α that are componentwise at most γ.

noncomputable def DistributionalKernels.iterCoordDeriv {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (j : Fin n) (m : ℕ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F

The m-fold distributional partial derivative in coordinate j, acting on a tempered distribution.

noncomputable def DistributionalKernels.multiIndexDistribDeriv {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (γ : Fin n → ℕ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F

The multi-index distributional derivative D^γ v, taken coordinate by coordinate.

noncomputable def DistributionalKernels.distribMulBracketPow {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (k : ℤ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F

Multiplication of a tempered distribution by the power ⟨x⟩^k of the Japanese bracket.

noncomputable def DistributionalKernels.distribMulPoly {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (p : MvPolynomial (Fin n) ℝ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F

Multiplication of a tempered distribution by a real polynomial evaluated at x.

noncomputable def DistributionalKernels.weightedDerivRHS {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (γ : Fin n → ℕ) (k : ℤ) (coeffs : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F

The right-hand side of the Leibniz expansion D^γ (p ⟨x⟩^k v): a sum over α ≤ γ of D^{γ-α} applied to polynomial-times-bracket-power multiples of v.

theorem DistributionalKernels.multiIndexDistribDeriv_zero {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : multiIndexDistribDeriv 0 v = v

D^0 v = v: the zero multi-index derivative is the identity.

theorem DistributionalKernels.distribMulPoly_one {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : distribMulPoly 1 v = v

Multiplication by the constant polynomial 1 leaves a tempered distribution unchanged.

theorem DistributionalKernels.multiIndexLeqFinset_zero {n : ℕ} : multiIndexLeqFinset 0 = {0}

For γ = 0, the set of multi-indices α ≤ γ is the singleton {0}.

theorem DistributionalKernels.iterCoordDeriv_zero {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (j : Fin n) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : iterCoordDeriv j 0 v = v

Zero iterations of a coordinate derivative leave the distribution unchanged.

theorem DistributionalKernels.iterCoordDeriv_succ {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (j : Fin n) (m : ℕ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : iterCoordDeriv j (m + 1) v = iterCoordDeriv j 1 (iterCoordDeriv j m v)

Inductive step: (m + 1) iterations equal one iteration applied to m iterations.

theorem DistributionalKernels.multiIndexSize_zero {n : ℕ} : multiIndexSize 0 = 0

The zero multi-index has size zero.

theorem DistributionalKernels.weightedDerivRHS_zero_eq {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (k : ℤ) (p : MvPolynomial (Fin n) ℝ) (coeffs : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ) (hc : coeffs 0 = p) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : weightedDerivRHS 0 k coeffs v = distribMulPoly p (distribMulBracketPow k v)

For γ = 0, the weighted derivative RHS reduces to plain polynomial-times-bracket multiplication.

theorem DistributionalKernels.distribDeriv_comm_general {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (v w : EuclideanSpace ℝ (Fin n)) (T : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : (TemperedDistributions.distribDerivCLM v) ((TemperedDistributions.distribDerivCLM w) T) = (TemperedDistributions.distribDerivCLM w) ((TemperedDistributions.distribDerivCLM v) T)

Directional distributional derivatives commute on F-valued tempered distributions.

theorem DistributionalKernels.iterCoordDeriv_one_comm_one {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (j₀ j : Fin n) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : iterCoordDeriv j₀ 1 (iterCoordDeriv j 1 v) = iterCoordDeriv j 1 (iterCoordDeriv j₀ 1 v)

Single applications of ∂_{j₀} and ∂_j commute.

theorem DistributionalKernels.iterCoordDeriv_one_comm {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (j₀ j : Fin n) (m : ℕ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : iterCoordDeriv j₀ 1 (iterCoordDeriv j m v) = iterCoordDeriv j m (iterCoordDeriv j₀ 1 v)

∂_{j₀} commutes with ∂_j^m for any m.

theorem DistributionalKernels.iterCoordDeriv_one_comm_foldl {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (j₀ : Fin n) (γ : Fin n → ℕ) (l : List (Fin n)) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : iterCoordDeriv j₀ 1 (List.foldl (fun (w : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) (j : Fin n) => iterCoordDeriv j (γ j) w) v l) = List.foldl (fun (w : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) (j : Fin n) => iterCoordDeriv j (γ j) w) (iterCoordDeriv j₀ 1 v) l

∂_{j₀} commutes with any foldl of iterated coordinate derivatives.

theorem DistributionalKernels.multiIndexDistribDeriv_step {n : ℕ} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℂ F] (γ : Fin n → ℕ) (j₀ : Fin n) (hj₀ : 0 < γ j₀) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : multiIndexDistribDeriv γ v = iterCoordDeriv j₀ 1 (multiIndexDistribDeriv (Function.update γ j₀ (γ j₀ - 1)) v)

Recursive step: peel off one factor of ∂_{j₀} from D^γ, reducing γ_{j₀} by one.

theorem DistributionalKernels.schwartz_product_rule_poly_bracket {n : ℕ} (j₀ : Fin n) (p : MvPolynomial (Fin n) ℝ) (k : ℤ) (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℂ F] (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : distribMulPoly p (distribMulBracketPow k (iterCoordDeriv j₀ 1 u)) = iterCoordDeriv j₀ 1 (distribMulPoly p (distribMulBracketPow k u)) - distribMulPoly (MvPolynomial.X j₀ * p) (distribMulBracketPow (k - 2) u)

Schwartz product rule for p · ⟨x⟩^k · ∂_{j₀} u: derivative is split between the polynomial-bracket factor and u.

theorem DistributionalKernels.distribMulPoly_bracketPow_deriv_expand {n : ℕ} (j₀ : Fin n) (p : MvPolynomial (Fin n) ℝ) (j : ℕ) (_hp : p.totalDegree ≤ j) (k : ℤ) (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℂ F] (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F) : distribMulPoly p (distribMulBracketPow k (iterCoordDeriv j₀ 1 u)) = iterCoordDeriv j₀ 1 (distribMulPoly p (distribMulBracketPow k u)) - distribMulPoly (MvPolynomial.X j₀ * p) (distribMulBracketPow (k - 2) u)

Expansion of p · ⟨x⟩^k · ∂_{j₀} u via the polynomial-bracket Schwartz product rule, with an explicit degree bound.

theorem DistributionalKernels.weightedDerivRHS_combine {n : ℕ} (γ γ' : Fin n → ℕ) (j₀ : Fin n) (hj₀ : 0 < γ j₀) (hγ' : γ' = Function.update γ j₀ (γ j₀ - 1)) (j : ℕ) (c₁ : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ) (hd₁ : ∀ α ≤ γ', (c₁ α).totalDegree ≤ j + multiIndexSize (γ' - α)) (hz₁ : ∀ (α : Fin n → ℕ), ¬α ≤ γ' → c₁ α = 0) (c₂ : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ) (hd₂ : ∀ α ≤ γ', (c₂ α).totalDegree ≤ j + 1 + multiIndexSize (γ' - α)) (hz₂ : ∀ (α : Fin n → ℕ), ¬α ≤ γ' → c₂ α = 0) : ∃ (coeffs : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ), (∀ α ≤ γ, (coeffs α).totalDegree ≤ j + multiIndexSize (γ - α)) ∧ (∀ (α : Fin n → ℕ), ¬α ≤ γ → coeffs α = 0) ∧ ∀ (F : Type u_2) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] (k : ℤ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F), iterCoordDeriv j₀ 1 (weightedDerivRHS γ' k c₁ v) - weightedDerivRHS γ' (k - 2) c₂ v = weightedDerivRHS γ k coeffs v

Combine two weightedDerivRHS expansions for γ' = γ-with-γ_{j₀}-1 into a single expansion for γ.

theorem DistributionalKernels.weighted_deriv_expansion_assemble {n : ℕ} (γ : Fin n → ℕ) (j : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ j) (j₀ : Fin n) (hj₀ : 0 < γ j₀) (γ' : Fin n → ℕ) (hγ'_def : γ' = Function.update γ j₀ (γ j₀ - 1)) (c₁ : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ) (hd₁ : ∀ α ≤ γ', (c₁ α).totalDegree ≤ j + multiIndexSize (γ' - α)) (hz₁ : ∀ (α : Fin n → ℕ), ¬α ≤ γ' → c₁ α = 0) (c₂ : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ) (hd₂ : ∀ α ≤ γ', (c₂ α).totalDegree ≤ j + 1 + multiIndexSize (γ' - α)) (hz₂ : ∀ (α : Fin n → ℕ), ¬α ≤ γ' → c₂ α = 0) : ∃ (coeffs : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ), (∀ α ≤ γ, (coeffs α).totalDegree ≤ j + multiIndexSize (γ - α)) ∧ (∀ (α : Fin n → ℕ), ¬α ≤ γ → coeffs α = 0) ∧ ∀ (F : Type u_2) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] (k : ℤ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F), iterCoordDeriv j₀ 1 (weightedDerivRHS γ' k c₁ v) - weightedDerivRHS γ' (k - 2) c₂ v = weightedDerivRHS γ k coeffs v

Assembly of the inductive step for the weighted derivative expansion (just weightedDerivRHS_combine repackaged with the polynomial hypothesis).

theorem DistributionalKernels.weighted_deriv_expansion {n : ℕ} (γ : Fin n → ℕ) (j : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ j) : ∃ (coeffs : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ), (∀ α ≤ γ, (coeffs α).totalDegree ≤ j + multiIndexSize (γ - α)) ∧ (∀ (α : Fin n → ℕ), ¬α ≤ γ → coeffs α = 0) ∧ ∀ (F : Type u_2) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] (k : ℤ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F), distribMulPoly p (distribMulBracketPow k (multiIndexDistribDeriv γ v)) = weightedDerivRHS γ k coeffs v

Full Leibniz-type expansion p · ⟨x⟩^k · D^γ v = ∑_{α ≤ γ} D^{γ-α} (coeffs α · ⟨x⟩^{k - 2|γ-α|} v) with polynomial degree bounds.

theorem DistributionalKernels.weighted_deriv_expansion_base {n : ℕ} (γ : Fin n → ℕ) : ∃ (coeffs : (Fin n → ℕ) → MvPolynomial (Fin n) ℝ), (∀ α ≤ γ, (coeffs α).totalDegree ≤ multiIndexSize (γ - α)) ∧ (∀ (α : Fin n → ℕ), ¬α ≤ γ → coeffs α = 0) ∧ ∀ (F : Type u_2) [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] (k : ℤ) (v : TemperedDistribution (EuclideanSpace ℝ (Fin n)) F), distribMulBracketPow k (multiIndexDistribDeriv γ v) = weightedDerivRHS γ k coeffs v

Base case p = 1: ⟨x⟩^k · D^γ v = ∑_{α ≤ γ} D^{γ-α}(coeffs α · ⟨x⟩^{k - 2|γ-α|} v).