Stat.Nonparametric.LocalPolynomial
General local-polynomial analysis: coordinate partial derivatives, operator-norm bounds, and coercivity of weighted radial polynomial energies.
CoordinateDerivative 4 core · 1 supporting This file represents bivariate multi-index partial derivatives by evaluating iterated Fréchet derivatives along repeated standard-coordinate directions, and bounds those evaluations by the multilinear operator norm. ★ coordinatePartial_abs_le_iteratedFDeriv_norm
Bivariate coordinate derivatives and operator-norm bounds
This file represents bivariate multi-index partial derivatives by evaluating iterated Fréchet derivatives along repeated standard-coordinate directions, and bounds those evaluations by the multilinear operator norm.
def coordinateMultiOrder reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a bivariate multi-index, the total order of that multi-index is the sum of its two coordinate orders.
Definition (Lean source)
def coordinateDirections reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a bivariate multi-index and a position in a list whose length is its total order, the associated ordered standard-coordinate direction is the first standard coordinate direction when the position is smaller than the first coordinate order, and the second standard coordinate direction otherwise.
Definition (Lean source)
def coordinatePartial reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a real-valued function on two-dimensional Euclidean space, a bivariate multi-index, and a point in that space, the scalar coordinate partial derivative is the iterated derivative of total order given by the multi-index, evaluated at the point along the associated ordered standard-coordinate directions.
Definition (Lean source)
parameters
def
coordinatePartial f alpha x :
ℝ
given by
lemma coordinatePartial_abs_le_iteratedFDeriv_norm reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
Evaluating the iterated Fréchet derivative of a function f along the standard coordinate directions given by a bivariate multi-index alpha at a point x, cannot increase its operator norm — the resulting scalar coordinate partial is bounded in absolute value by the operator norm of the full iterated derivative.
Formal statement
hypotheses
conclusion
|coordinatePartial f alpha x| ≤ ‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x‖
Proof (Lean source)
lemma coordinatePartial_abs_le_iteratedFDeriv_norm
(f : EuclideanSpace ℝ (Fin 2) → ℝ) (alpha : Fin 2 → ℕ) (x : EuclideanSpace ℝ (Fin 2)) :
|coordinatePartial f alpha x| ≤
‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x‖ := by
unfold coordinatePartial
have h := (iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x).le_opNorm
(coordinateDirections alpha)
have hprod : ∏ k : Fin (coordinateMultiOrder alpha),
‖coordinateDirections alpha k‖ ≤ 1 := by
simpa using Finset.prod_le_one (fun _ _ ↦ norm_nonneg _)
(fun k _ ↦ by
unfold coordinateDirections
split <;> simp [EuclideanSpace.norm_single])
simpa only [Real.norm_eq_abs, mul_one] using
h.trans (mul_le_mul_of_nonneg_left hprod (norm_nonneg _))
1 supporting declaration (lemmas, instances)
-
coordinatePartial_sub_abs_le_iteratedFDeriv_sub_normlemma — Differences of scalar coordinate partials are bounded by the operator norm of the corresponding Fréchet-derivative difference.hypothesesconclusion|coordinatePartial f alpha x - coordinatePartial f alpha z|≤ ‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x - iteratedFDeriv ℝ (coordinateMultiOrder alpha) f z‖Proof (Lean source)
lemma coordinatePartial_sub_abs_le_iteratedFDeriv_sub_norm (f : EuclideanSpace ℝ (Fin 2) → ℝ) (alpha : Fin 2 → ℕ) (x z : EuclideanSpace ℝ (Fin 2)) : |coordinatePartial f alpha x - coordinatePartial f alpha z| ≤ ‖iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x - iteratedFDeriv ℝ (coordinateMultiOrder alpha) f z‖ := by unfold coordinatePartial rw [← ContinuousMultilinearMap.sub_apply] have h := (iteratedFDeriv ℝ (coordinateMultiOrder alpha) f x - iteratedFDeriv ℝ (coordinateMultiOrder alpha) f z).le_opNorm (coordinateDirections alpha) have hprod : ∏ k : Fin (coordinateMultiOrder alpha), ‖coordinateDirections alpha k‖ ≤ 1 := by simpa using Finset.prod_le_one (fun _ _ ↦ norm_nonneg _) (fun k _ ↦ by unfold coordinateDirections split <;> simp [EuclideanSpace.norm_single]) simpa only [Real.norm_eq_abs, mul_one] using h.trans (mul_le_mul_of_nonneg_left hprod (norm_nonneg _))
GramCoercivity 3 core · 7 supporting This file represents finite local-polynomial coefficient vectors as polynomials and proves a positive, dimension-dependent lower bound for their weighted squared moment on a nondegenerate radial interval. ★ radialPolynomialEnergy_coercive
Coercivity of local-polynomial moment matrices
This file represents finite local-polynomial coefficient vectors as polynomials and proves a positive, dimension-dependent lower bound for their weighted squared moment on a nondegenerate radial interval.
def localPolynomial reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a nonnegative polynomial degree and real coefficients indexed from zero through that degree, the local-polynomial coefficient polynomial is .
Definition (Lean source)
parameters
p :
ℕ
v :
Fin (p + 1) → ℝ
def
localPolynomial p v :
ℝ[X]
given by
∑ i, Polynomial.C (v i) * Polynomial.X ^ (i : ℕ)
def radialPolynomialEnergy reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a nonnegative polynomial degree and real coefficients indexed from zero through that degree, the radial polynomial energy is the double sum of divided by , over all coefficient indices from zero through that degree.
lemma radialPolynomialEnergy_coercive reviewed
⚑ flagged
Causalean.Stat.Nonparametric.LocalPolynomial
For a polynomial degree bound p, there is a positive constant such that the radial polynomial energy of any coefficient vector is bounded below by that constant times the sum of the squared coefficients: on the unit sphere of the sup norm on coefficient vectors, radial polynomial energy has a positive minimum, and homogeneity packages this as a coercive lower bound for all coefficient vectors.
Formal statement
hypotheses
p :
ℕ
conclusion
∃ c : ℝ,
0 < c
Proof (Lean source)
lemma radialPolynomialEnergy_coercive (p : ℕ) :
∃ c : ℝ, 0 < c ∧ ∀ v : Fin (p + 1) → ℝ,
c * ∑ i, (v i) ^ 2 ≤ radialPolynomialEnergy p v := by
let S : Set (Fin (p + 1) → ℝ) := sphere 0 1
have hScompact : IsCompact S := isCompact_sphere 0 1
have hSne : S.Nonempty := by
refine ⟨fun _i => 1, ?_⟩
rw [Metric.mem_sphere, dist_zero_right]
simpa using (pi_norm_const' (ι := Fin (p + 1)) (1 : ℝ))
obtain ⟨v0, hv0S, hv0min⟩ := hScompact.exists_isMinOn hSne
(radialPolynomialEnergy_continuous p).continuousOn
have hv0ne : v0 ≠ 0 := by
intro h
subst v0
simpa [S] using hv0S
let c := radialPolynomialEnergy p v0 / (p + 1 : ℝ)
have hqpos : (0 : ℝ) < p + 1 := by positivity
refine ⟨c, div_pos (radialPolynomialEnergy_pos p hv0ne) hqpos, ?_⟩
intro v
by_cases hv : v = 0
· subst v
simp [radialPolynomialEnergy]
· let r : ℝ := ‖v‖
have hrpos : 0 < r := norm_pos_iff.mpr hv
let u : Fin (p + 1) → ℝ := r⁻¹ • v
have huS : u ∈ S := by
rw [Metric.mem_sphere, dist_zero_right]
change ‖r⁻¹ • v‖ = 1
rw [norm_smul, Real.norm_eq_abs, abs_inv, abs_of_pos hrpos]
exact inv_mul_cancel₀ hrpos.ne'
have hmin := hv0min huS
have hscale := radialPolynomialEnergy_smul p r u
have hru : r • u = v := by
ext i
simp [u, r, hrpos.ne']
rw [hru] at hscale
have hsum : ∑ i, (v i) ^ 2 ≤ (p + 1 : ℝ) * r ^ 2 := by
calc
∑ i, (v i) ^ 2 ≤ ∑ _i : Fin (p + 1), r ^ 2 := by
apply Finset.sum_le_sum
intro i hi
simpa [sq_abs, r] using
(sq_le_sq₀ (abs_nonneg (v i)) (norm_nonneg v)).2
(norm_le_pi_norm v i)
_ = (p + 1 : ℝ) * r ^ 2 := by simp
dsimp [c]
calc
radialPolynomialEnergy p v0 / (p + 1 : ℝ) * ∑ i, (v i) ^ 2
= radialPolynomialEnergy p v0 *
((∑ i, (v i) ^ 2) / (p + 1 : ℝ)) := by ring
_ ≤ radialPolynomialEnergy p v0 * r ^ 2 := by
apply mul_le_mul_of_nonneg_left _ (radialPolynomialEnergy_pos p hv0ne).le
exact (div_le_iff₀ hqpos).2 (by simpa [mul_comm] using hsum)
_ ≤ radialPolynomialEnergy p u * r ^ 2 := by
exact mul_le_mul_of_nonneg_right hmin (sq_nonneg r)
_ = radialPolynomialEnergy p v := by
rw [mul_comm, ← hscale]
7 supporting declarations (lemmas, instances)
-
localPolynomial_evallemma — Evaluation of the coefficient polynomial is the dot product with the monomial basis.hypothesesconclusion(localPolynomial p v).eval u = ∑ i, v i * u ^ (i : ℕ)Proof (Lean source)
lemma localPolynomial_eval (p : ℕ) (v : Fin (p + 1) → ℝ) (u : ℝ) : (localPolynomial p v).eval u = ∑ i, v i * u ^ (i : ℕ) := by simp only [localPolynomial, Polynomial.eval_finset_sum, Polynomial.eval_mul, Polynomial.eval_C, Polynomial.eval_pow, Polynomial.eval_X] -
localPolynomial_eq_zero_ifflemma — The coefficient polynomial vanishes only when every coefficient does.Proof (Lean source)
lemma localPolynomial_eq_zero_iff (p : ℕ) (v : Fin (p + 1) → ℝ) : localPolynomial p v = 0 ↔ v = 0 := by constructor · intro hp funext i have hc := congrArg (fun q : ℝ[X] => q.coeff (i : ℕ)) hp simp only [localPolynomial, Polynomial.finset_sum_coeff, Polynomial.coeff_C_mul_X_pow] at hc rw [Finset.sum_eq_single i] at hc · simpa using hc · intro j hj hji have hne : (i : ℕ) ≠ (j : ℕ) := by intro hij exact hji (Fin.ext hij.symm) simp [hne] · simp · rintro rfl simp [localPolynomial] -
radialPolynomialEnergy_eq_integrallemma — The explicit moment matrix is exactly the weighted squared-polynomial integral on the unit interval.hypothesesp :ℕv :Fin (p + 1) → ℝconclusionradialPolynomialEnergy p v = ∫ u in (0 : ℝ)..1, (∑ i, v i * u ^ (i : ℕ)) ^ 2 * uProof (Lean source)
lemma radialPolynomialEnergy_eq_integral (p : ℕ) (v : Fin (p + 1) → ℝ) : radialPolynomialEnergy p v = ∫ u in (0 : ℝ)..1, (∑ i, v i * u ^ (i : ℕ)) ^ 2 * u := by rw [radialPolynomialEnergy] simp_rw [pow_two, Fintype.sum_mul_sum] simp_rw [Finset.sum_mul] rw [intervalIntegral.integral_finset_sum] apply Finset.sum_congr rfl intro i hi rw [intervalIntegral.integral_finset_sum] apply Finset.sum_congr rfl intro j hj rw [show (fun u : ℝ => (v i * u ^ (i : ℕ)) * (v j * u ^ (j : ℕ)) * u) = fun u => (v i * v j) * u ^ ((i : ℕ) + (j : ℕ) + 1) by funext u; rw [pow_add]; ring] rw [intervalIntegral.integral_const_mul, integral_pow] · push_cast ring all_goals intros apply Continuous.intervalIntegrable fun_prop -
radialPolynomialEnergy_poslemma — A nonzero coefficient vector has strictly positive radial energy.Proof (Lean source)
lemma radialPolynomialEnergy_pos (p : ℕ) {v : Fin (p + 1) → ℝ} (hv : v ≠ 0) : 0 < radialPolynomialEnergy p v := by let f : ℝ → ℝ := fun u => (∑ i, v i * u ^ (i : ℕ)) ^ 2 * u have hfcont : Continuous f := by fun_prop have hfint : IntervalIntegrable f volume 0 1 := hfcont.intervalIntegrable 0 1 rw [radialPolynomialEnergy_eq_integral] have hpoly : localPolynomial p v ≠ 0 := by simpa [localPolynomial_eq_zero_iff] using hv have hroots : Finite {u : ℝ | Polynomial.IsRoot (localPolynomial p v) u} := (Polynomial.roots (localPolynomial p v)).toFinset.finite_toSet.subset (by intro u hu simpa [Polynomial.mem_roots hpoly] using hu) have hinter : Set.Infinite (Ioo (0 : ℝ) 1) := Set.Ioo_infinite (by norm_num) obtain ⟨u, huI, huroot⟩ := (hinter.diff hroots).nonempty have hune : (∑ i, v i * u ^ (i : ℕ)) ≠ 0 := by rw [← localPolynomial_eval] intro he exact huroot (by simpa [Polynomial.IsRoot] using he) have hfu : f u ≠ 0 := mul_ne_zero (pow_ne_zero 2 hune) (ne_of_gt huI.1) rw [intervalIntegral.integral_pos_iff_support_of_nonneg_ae' (by filter_upwards [ae_restrict_mem (measurableSet_uIoc : MeasurableSet (Set.uIoc (0 : ℝ) 1))] with x hx rw [Set.uIoc_of_le (by norm_num)] at hx have hx0 : 0 ≤ x := by exact hx.1.le change 0 ≤ (∑ i, v i * x ^ (i : ℕ)) ^ 2 * x exact mul_nonneg (sq_nonneg _) hx0) hfint] refine ⟨by norm_num, ?_⟩ let U := support f ∩ Ioo (0 : ℝ) 1 have hUopen : IsOpen U := hfcont.isOpen_support.inter isOpen_Ioo have hUne : U.Nonempty := ⟨u, hfu, huI⟩ exact lt_of_lt_of_le (hUopen.measure_pos volume hUne) (measure_mono (by intro x hx exact ⟨hx.1, hx.2.1, hx.2.2.le⟩)) -
radialPolynomialEnergy_continuouslemma — The radial energy is a continuous quadratic function of its coefficient vector.Proof (Lean source)
@[fun_prop] lemma radialPolynomialEnergy_continuous (p : ℕ) : Continuous (radialPolynomialEnergy p) := by unfold radialPolynomialEnergy fun_prop -
radialPolynomialEnergy_smullemma — Radial energy is homogeneous of degree two in the coefficient vector.hypothesesconclusionradialPolynomialEnergy p (a • v) = a ^ 2 * radialPolynomialEnergy p vProof (Lean source)
lemma radialPolynomialEnergy_smul (p : ℕ) (a : ℝ) (v : Fin (p + 1) → ℝ) : radialPolynomialEnergy p (a • v) = a ^ 2 * radialPolynomialEnergy p v := by unfold radialPolynomialEnergy rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i hi rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj simp only [Pi.smul_apply, smul_eq_mul] ring -
signedRadialPolynomialEnergy_coercivelemma — The same coercivity constant works in both signed-distance orientations. The negative orientation merely changes coefficient i by the sign (-1)^i, which preserves the sum of coefficient squares.hypothesesp :ℕProof (Lean source)
lemma signedRadialPolynomialEnergy_coercive (p : ℕ) : ∃ c : ℝ, 0 < c ∧ ∀ t : Bool, ∀ v : Fin (p + 1) → ℝ, c * ∑ i, (v i) ^ 2 ≤ ∫ u in (0 : ℝ)..1, (∑ i, v i * (if t then u else -u) ^ (i : ℕ)) ^ 2 * u := by obtain ⟨c, hc, hcoercive⟩ := radialPolynomialEnergy_coercive p refine ⟨c, hc, ?_⟩ intro t v cases t with | true => simpa [radialPolynomialEnergy_eq_integral] using hcoercive v | false => let w : Fin (p + 1) → ℝ := fun i => (-1 : ℝ) ^ (i : ℕ) * v i have hnorm : ∑ i, (w i) ^ 2 = ∑ i, (v i) ^ 2 := by apply Finset.sum_congr rfl intro i hi simp only [w, mul_pow] rw [show ((-1 : ℝ) ^ (i : ℕ)) ^ 2 = 1 by rw [← pow_mul]; simp] ring have hpoly (u : ℝ) : ∑ i, w i * u ^ (i : ℕ) = ∑ i, v i * (-u) ^ (i : ℕ) := by apply Finset.sum_congr rfl intro i hi simp only [w] rw [neg_pow] ring rw [← hnorm] refine (hcoercive w).trans_eq ?_ rw [radialPolynomialEnergy_eq_integral] apply intervalIntegral.integral_congr intro u hu dsimp only simp only [Bool.false_eq_true, ↓reduceIte] rw [hpoly]