Stat.Nonparametric.Approximation.Holder­Interpolation

The canonical Tsybakov nonparametric-minimax lower-bound primitive.

Holder­Interpolation 1 core · 1 supporting The canonical Tsybakov nonparametric-minimax lower-bound primitive. ★ holder_point_l1_interpolation

Hölder pointwise ⟹ local L¹ mass (main primitive)

The canonical Tsybakov nonparametric-minimax lower-bound primitive. For a function g in a multivariate Hölder ball of order γ and radius M, a pointwise value |g x0| forces a local L¹ mass lower bound on the cube supBall x0 r: ∫_{supBall x0 r} |g| ≥ c_H · |g x0|^{1 + d/γ}, with c_H > 0 depending only on γ, d, M, r (uniform over the whole Hölder ball).

Proof (standard Tsybakov, three milestones)

1. Moment-cancelling product kernel (Kernel.lean): from exists_moment_cancelling_kernel_1d m (with m = ⌈γ⌉₊ - 1) get a bounded, [-1,1]-supported 1-D kernel k with unit mass and vanishing moments up to m; tensorize to K = prodKernel k d. Fubini over the product Lebesgue measure gives ∫_{[-1,1]^d} K = 1 and ∫ uᵛ K(u) du = 0 for 1 ≤ |ν| ≤ m. 2. Taylor + moment cancellation: for 0 < h ≤ r, multivariate Taylor of g at x0 to order m with the integer-order Hölder remainder plus the moment cancellations bounds the kernel bias |g(x0) - ∫ h⁻ᵈ K((x-x0)/h) g(x) dx| ≤ C_{γ,d} · M · hᵞ. 3. Optimize h (l1_lower_of_bias_bound): with Δ = |g x0|, choose h = c_* Δ^{1/γ} so the remainder is ≤ Δ/4; then 3Δ/4 ≤ ‖K‖_∞ h⁻ᵈ ∫_{supBall x0 r} |g|, and rearranging yields the Δ^{1 + d/γ} lower bound. The Δ = 0 case is immediate (RHS ≥ 0).

theorem holder_point_l1_interpolation reviewed
Causalean.Stat.Nonparametric

Hölder pointwise ⟹ local L¹ mass interpolation. Fix a point x0 in d-dimensional Euclidean space. If the Hölder exponent γ is positive, the Hölder constant M is positive, the neighbourhood radius r is positive, and the sup-norm ball of radius r around x0 is contained in the domain S, then there is a constant c_H > 0, depending only on γ, d, M, r and uniform over the Hölder ball, such that every function g in the standard Hölder ball of exponent γ, constant M, and domain S satisfies c_H · |g(x0)|^{1 + d/γ} ≤ ∫_{supBall x0 r} |g|.

Formal statement
hypotheses
d :
ℕ
γ M r :
ℝ
x0 :
Fin d → ℝ
S :
Set (Fin d → ℝ)
hγ :
0 < γ
hM :
0 < M
hr :
0 < r
hS :
supBall x0 r ⊆ S
conclusion
∃ cH : ℝ
if
0 < cH ∧ ∀ g : (Fin d → ℝ)
and
ℝ, HolderBallStd g γ M S
then
cH * |g x0| ^ (1 + (d : ℝ) / γ) ≤ ∫ x in supBall x0 r, |g x|
Proof (Lean source)
theorem holder_point_l1_interpolation {d : ℕ} {γ M r : ℝ} {x0 : Fin d → ℝ} {S : Set (Fin d → ℝ)} (hγ : 0 < γ) (hM : 0 < M) (hr : 0 < r) (hS : supBall x0 r ⊆ S) : ∃ cH : ℝ, 0 < cH ∧ ∀ g : (Fin d → ℝ) → ℝ, HolderBallStd g γ M S → cH * |g x0| ^ (1 + (d : ℝ) / γ) ≤ ∫ x in supBall x0 r, |g x| := by classical -- Milestone 1: the moment-cancelling 1-D kernel and its tensorization `K = prodKernel k d`. obtain ⟨k, hk_cont, hk_supp, hk_mass, hk_mom⟩ := exists_moment_cancelling_kernel_1d (⌈γ⌉₊ - 1) -- `k` is bounded (continuous with support in `[-1,1]`). have hcs : HasCompactSupport k := by apply HasCompactSupport.intro (isCompact_Icc (a := (-1 : ℝ)) (b := 1)) intro x hx apply hk_supp rw [Set.mem_Icc, not_and_or] at hx rcases hx with hx | hx · rw [not_le] at hx; rw [lt_abs]; right; linarith · rw [not_le] at hx; rw [lt_abs]; left; linarith obtain ⟨C0, hC0⟩ := hk_cont.bounded_above_of_compact_support hcs set B := max C0 0 with hBdef have hB : ∀ u, |k u| ≤ B := fun u => le_trans (by simpa [Real.norm_eq_abs] using hC0 u) (le_max_left _ _) have hB0 : 0 ≤ B := le_max_right _ _ -- `B > 0`: else `k ≡ 0`, contradicting unit mass. have hBpos : 0 < B := by rcases hB0.lt_or_eq with h | h · exact h · exfalso have hk0 : ∀ u, k u = 0 := by intro u have hle : |k u| ≤ 0 := by rw [h]; exact hB u exact abs_eq_zero.mp (le_antisymm hle (abs_nonneg _)) rw [MeasureTheory.setIntegral_congr_fun measurableSet_Icc (fun u _ => hk0 u)] at hk_mass simp at hk_mass have hBd : 0 < B ^ d := pow_pos hBpos d -- Milestone 2: the uniform bias constant `C`. obtain ⟨C, hC0nn, hCbias⟩ := holder_taylor_bias hγ hM hr hS hk_cont hk_supp hk_mass hk_mom hB hB0 -- Milestone 3: choose the optimal bandwidth constant `cstar`. have hMrpow_pos : 0 < M ^ ((1 : ℝ) / γ) := Real.rpow_pos_of_pos hM _ have hC1 : (0 : ℝ) < C + 1 := by positivity have hden_pos : (0 : ℝ) < 4 * (C + 1) * M := by positivity have hb_pos : 0 < (1 / (4 * (C + 1) * M)) ^ ((1 : ℝ) / γ) := Real.rpow_pos_of_pos (by positivity) _ set cstar := min (r / M ^ ((1 : ℝ) / γ)) ((1 / (4 * (C + 1) * M)) ^ ((1 : ℝ) / γ)) with hcstar_def have hcstar_pos : 0 < cstar := lt_min (div_pos hr hMrpow_pos) hb_pos refine ⟨(3 / (4 * B ^ d)) * cstar ^ d, ?_, ?_⟩ · exact mul_pos (div_pos (by norm_num) (mul_pos (by norm_num) hBd)) (pow_pos hcstar_pos d) · intro g hg set Δ := |g x0| with hΔdef have hΔnn : 0 ≤ Δ := by rw [hΔdef]; exact abs_nonneg _ rcases hΔnn.lt_or_eq with hΔpos | hΔ0 swap · -- `Δ = 0`: RHS ≥ 0. rw [← hΔ0, Real.zero_rpow (by positivity : (1 : ℝ) + (d : ℝ) / γ ≠ 0), mul_zero] exact MeasureTheory.setIntegral_nonneg (measurableSet_supBall x0 r) (fun x _ => abs_nonneg _) · -- `Δ > 0`. have hx0S : x0 ∈ S := hS (mem_supBall_self x0 hr.le) have hΔM : Δ ≤ M := by have h0 := hg.2.1 0 (zero_le _) x0 hx0S rw [norm_iteratedFDeriv_zero, Real.norm_eq_abs] at h0 rw [hΔdef]; exact h0 set h := cstar * Δ ^ ((1 : ℝ) / γ) with hh_def have hh_pos : 0 < h := mul_pos hcstar_pos (Real.rpow_pos_of_pos hΔpos _) -- `h ≤ r`. have hh_le_r : h ≤ r := by rw [hh_def] have hΔle : Δ ^ ((1 : ℝ) / γ) ≤ M ^ ((1 : ℝ) / γ) := Real.rpow_le_rpow hΔnn hΔM (one_div_nonneg.mpr hγ.le) have hne := hMrpow_pos.ne' calc cstar * Δ ^ ((1 : ℝ) / γ) ≤ cstar * M ^ ((1 : ℝ) / γ) := mul_le_mul_of_nonneg_left hΔle hcstar_pos.le _ ≤ (r / M ^ ((1 : ℝ) / γ)) * M ^ ((1 : ℝ) / γ) := mul_le_mul_of_nonneg_right (min_le_left _ _) hMrpow_pos.le _ = r := by field_simp -- Remainder `C·M·hᵞ ≤ Δ/4`. have hpow : (Δ ^ ((1 : ℝ) / γ)) ^ γ = Δ := by rw [← Real.rpow_mul hΔnn, one_div_mul_cancel hγ.ne', Real.rpow_one] have hhg : h ^ γ = cstar ^ γ * Δ := by rw [hh_def, Real.mul_rpow hcstar_pos.le (Real.rpow_nonneg hΔnn _), hpow] have hcstar_g : cstar ^ γ ≤ 1 / (4 * (C + 1) * M) := by have h2 : cstar ^ γ ≤ ((1 / (4 * (C + 1) * M)) ^ ((1 : ℝ) / γ)) ^ γ := Real.rpow_le_rpow hcstar_pos.le (min_le_right _ _) hγ.le rwa [← Real.rpow_mul (by positivity), one_div_mul_cancel hγ.ne', Real.rpow_one] at h2 have hrem : C * M * h ^ γ ≤ Δ / 4 := by have hge : C * M * cstar ^ γ ≤ C * M * (1 / (4 * (C + 1) * M)) := mul_le_mul_of_nonneg_left hcstar_g (by positivity) have heq : C * M * (1 / (4 * (C + 1) * M)) = C / (4 * (C + 1)) := by field_simp rw [heq] at hge have hle14 : C / (4 * (C + 1)) ≤ 1 / 4 := by rw [div_le_iff₀ (by positivity : (0:ℝ) < 4 * (C + 1))]; nlinarith [hC0nn] have hCMc : C * M * cstar ^ γ ≤ 1 / 4 := le_trans hge hle14 rw [hhg] calc C * M * (cstar ^ γ * Δ) = (C * M * cstar ^ γ) * Δ := by ring _ ≤ (1 / 4) * Δ := mul_le_mul_of_nonneg_right hCMc hΔnn _ = Δ / 4 := by ring -- Bias and change-of-variables combine into the `l1` hypothesis. have hbias := hCbias g hg h hh_pos hh_le_r have hbias' : |g x0 - ∫ u in supBall (0 : Fin d → ℝ) 1, prodKernel k d u * g (x0 + h • u)| ≤ Δ / 4 := le_trans hbias hrem have hVlow : 3 * Δ / 4 ≤ |∫ u in supBall (0 : Fin d → ℝ) 1, prodKernel k d u * g (x0 + h • u)| := by have h1 := abs_sub_abs_le_abs_sub (g x0) (∫ u in supBall (0 : Fin d → ℝ) 1, prodKernel k d u * g (x0 + h • u)) rw [← hΔdef] at h1 linarith [le_trans h1 hbias'] have hsm := smoothed_abs_le hr hS (prodKernel_abs_le hB) g hg h hh_pos hh_le_r have hbound : 3 * Δ / 4 ≤ B ^ d * h⁻¹ ^ d * ∫ x in supBall x0 r, |g x| := le_trans hVlow hsm have hfin := l1_lower_of_bias_bound hγ hBd hΔpos hcstar_pos hh_def hbound rw [hΔdef] exact hfin
Causalean.Stat.Nonparametric.holder_point_l1_interpolation · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation.lean:795 · uses HolderBallStd , supBall
1 supporting declaration (lemmas, instances)
  • l1_lower_of_bias_bound theorem — The bandwidth optimization converts a lower bound on a kernel-smoothed signal into the Hölder interpolation rate: local absolute mass grows at least as the pointwise signal to the power one plus dimension divided by smoothness.
    hypotheses
    d :
    ℕ
    γ Ksup Δ Ival cstar h :
    ℝ
    _hγ :
    0 < γ
    hKsup :
    0 < Ksup
    hΔ :
    0 < Δ
    hcstar :
    0 < cstar
    hheq :
    h = cstar * Δ ^ ((1 : ℝ) / γ)
    hbound :
    3 * Δ / 4 ≤ Ksup * h⁻¹ ^ d * Ival
    conclusion
    (3 / (4 * Ksup)) * cstar ^ d * Δ ^ (1 + (d : ℝ) / γ) ≤ Ival
    Proof (Lean source)
    theorem l1_lower_of_bias_bound {d : ℕ} {γ Ksup Δ Ival cstar h : ℝ} (_hγ : 0 < γ) (hKsup : 0 < Ksup) (hΔ : 0 < Δ) (hcstar : 0 < cstar) (hheq : h = cstar * Δ ^ ((1 : ℝ) / γ)) (hbound : 3 * Δ / 4 ≤ Ksup * h⁻¹ ^ d * Ival) : (3 / (4 * Ksup)) * cstar ^ d * Δ ^ (1 + (d : ℝ) / γ) ≤ Ival := by have hqpos : (0 : ℝ) < Δ ^ ((d : ℝ) / γ) := Real.rpow_pos_of_pos hΔ _ have hcpos : 0 < cstar ^ d := pow_pos hcstar _ have hABpos : 0 < cstar ^ d * Δ ^ ((d : ℝ) / γ) := mul_pos hcpos hqpos -- `h ^ d = cstar ^ d * Δ ^ (d/γ)`. have hpow : h ^ d = cstar ^ d * Δ ^ ((d : ℝ) / γ) := by have h1 : (Δ ^ ((1 : ℝ) / γ)) ^ d = Δ ^ ((d : ℝ) / γ) := by rw [← Real.rpow_natCast (Δ ^ ((1 : ℝ) / γ)) d, ← Real.rpow_mul hΔ.le] congr 1 ring rw [hheq, mul_pow, h1] -- Rewrite the hypothesis with the explicit `h ^ d`. rw [inv_pow, hpow] at hbound -- Clear the inverse: `(3Δ/4)·(cstar^d·Δ^{d/γ}) ≤ Ksup·Ival`. have hmul : 3 * Δ / 4 * (cstar ^ d * Δ ^ ((d : ℝ) / γ)) ≤ Ksup * Ival := by have h2 := mul_le_mul_of_nonneg_right hbound hABpos.le have e : Ksup * (cstar ^ d * Δ ^ ((d : ℝ) / γ))⁻¹ * Ival * (cstar ^ d * Δ ^ ((d : ℝ) / γ)) = Ksup * Ival := by field_simp rwa [e] at h2 -- `Δ ^ (1 + d/γ) = Δ · Δ ^ (d/γ)`. have hΔadd : Δ ^ (1 + (d : ℝ) / γ) = Δ * Δ ^ ((d : ℝ) / γ) := by rw [Real.rpow_add hΔ, Real.rpow_one] have goaleq : (3 / (4 * Ksup)) * cstar ^ d * (Δ * Δ ^ ((d : ℝ) / γ)) = (3 * Δ / 4 * (cstar ^ d * Δ ^ ((d : ℝ) / γ))) / Ksup := by field_simp rw [hΔadd, goaleq, div_le_iff₀ hKsup, mul_comm Ival Ksup] exact hmul
    Causalean.Stat.Nonparametric.l1_lower_of_bias_bound · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation.lean:47
Defs 5 core · 5 supporting This module fixes the *generic* (estimand-agnostic) vocabulary for the Tsybakov nonparametric-minimax lower-bound primitive holder_point_l1_interpolation: for a function in a multivariate Hölder ball, a pointwise value f ★ isCompact_supBall★ volume_supBall

Generic multivariate Hölder ball and moment-cancelling product kernel — definitions

This module fixes the generic (estimand-agnostic) vocabulary for the Tsybakov nonparametric-minimax lower-bound primitive holder_point_l1_interpolation: for a function in a multivariate Hölder ball, a pointwise value forces a local L¹ mass lower bound via a moment-cancelling kernel.

The definitions are estimand-agnostic: they apply to any regression or response function and carry no dependency on a causal-law or treatment-effect type. This makes the primitive reusable in every Hölder-class two-point or Assouad lower bound.

* supBall x0 r — the sup-norm r-neighbourhood (closed cube) around x0, together with its basic geometry/measure API (supBall_eq_pi, isCompact_supBall, measurableSet_supBall, mem_supBall_self, volume_supBall). * HolderBallStd f γ M S — the standard ⌈γ⌉-1-convention multivariate Hölder ball of order γ, radius M, on S. * prodKernel k d — the tensorized product kernel u ↦ ∏ᵢ k (u i). * mem_cube, isCompact_cube — the same two facts for the axis-aligned box [a,b]^d, the other cube shape that shows up in Hölder-class lower bounds.

def supBall reviewed
Causalean.Stat.Nonparametric

The closed coordinatewise neighbourhood of radius r around a point: the cube containing exactly the covariate values whose every coordinate is within r of the corresponding coordinate of the centre.

Definition (Lean source)
def supBall {d : ℕ} (x0 : Fin d → ℝ) (r : ℝ) : Set (Fin d → ℝ) := {x | ∀ i, |x i - x0 i| ≤ r}
Causalean.Stat.Nonparametric.supBall · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:40
lemma isCompact_supBall reviewed
Causalean.Stat.Nonparametric

A closed sup-norm ball — the axis-aligned cube, or box, of half-width r centred at a point x0 in d-dimensional space — is compact, being a finite product of closed bounded intervals.

Formal statement
hypotheses
d :
ℕ
x0 :
Fin d → ℝ
r :
ℝ
conclusion
IsCompact (supBall x0 r)
Proof (Lean source)
lemma isCompact_supBall {d : ℕ} (x0 : Fin d → ℝ) (r : ℝ) : IsCompact (supBall x0 r) := by rw [supBall_eq_pi]; exact isCompact_univ_pi (fun _ => isCompact_Icc)
Causalean.Stat.Nonparametric.isCompact_supBall · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:56 · uses supBall
lemma volume_supBall reviewed
Causalean.Stat.Nonparametric

The Lebesgue volume of a closed sup-norm ball — the axis-aligned cube of side 2r centred at x0 in d dimensions — equals the d-th power of the side length, (2r)^d. No sign restriction on r is needed: a negative half-width gives an empty cube and a zero right-hand side.

Formal statement
hypotheses
d :
ℕ
x0 :
Fin d → ℝ
r :
ℝ
conclusion
volume (supBall x0 r) = ofReal (2 * r) ^ d
Proof (Lean source)
lemma volume_supBall {d : ℕ} (x0 : Fin d → ℝ) (r : ℝ) : volume (supBall x0 r) = ofReal (2 * r) ^ d := by rw [supBall_eq_pi, Set.pi_univ_Icc, Real.volume_Icc_pi] simp_rw [show ∀ i : Fin d, x0 i + r - (x0 i - r) = 2 * r from fun i => by ring] simp
Causalean.Stat.Nonparametric.volume_supBall · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:74 · uses supBall
def HolderBallStd reviewed
Causalean.Stat.Nonparametric

The standard multivariate Hölder ball of a given smoothness order and radius on a region: derivatives through the conventional highest order are continuous and bounded, and the highest derivative changes at the Hölder rate set by that order.

Definition (Lean source)
def HolderBallStd {d : ℕ} (f : (Fin d → ℝ) → ℝ) (order M : ℝ) (S : Set (Fin d → ℝ)) : Prop := ContDiffOn ℝ (⌈order⌉₊ - 1) f S ∧ (∀ j : ℕ, j ≤ ⌈order⌉₊ - 1 → ∀ x ∈ S, ‖iteratedFDeriv ℝ j f x‖ ≤ M) ∧ (∀ x ∈ S, ∀ y ∈ S, ‖iteratedFDeriv ℝ (⌈order⌉₊ - 1) f x - iteratedFDeriv ℝ (⌈order⌉₊ - 1) f y‖ ≤ M * ‖x - y‖ ^ (order - ((⌈order⌉₊ - 1 : ℕ) : ℝ)))
Causalean.Stat.Nonparametric.HolderBallStd · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:97
def prodKernel reviewed
Causalean.Stat.Nonparametric

The multivariate product kernel obtained by multiplying the same one-dimensional kernel across all covariate coordinates.

Definition (Lean source)
def prodKernel (k : ℝ → ℝ) (d : ℕ) : (Fin d → ℝ) → ℝ := fun u => ∏ i : Fin d, k (u i)
Causalean.Stat.Nonparametric.prodKernel · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:108
5 supporting declarations (lemmas, instances)
  • supBall_eq_pi lemma — A closed sup-norm ball — the axis-aligned cube of half-width r centred at a point — is exactly the product of the coordinate intervals of radius r around the centre's coordinates.
    hypotheses
    d :
    ℕ
    x0 :
    Fin d → ℝ
    r :
    ℝ
    conclusion
    supBall x0 r = Set.univ.pi (fun i => Icc (x0 i - r) (x0 i + r))
    Proof (Lean source)
    lemma supBall_eq_pi {d : ℕ} (x0 : Fin d → ℝ) (r : ℝ) : supBall x0 r = Set.univ.pi (fun i => Icc (x0 i - r) (x0 i + r)) := by ext x simp only [supBall, Set.mem_setOf_eq, Set.mem_univ_pi, Set.mem_Icc] refine ⟨fun h i => ?_, fun h i => ?_⟩ · have := (abs_le).mp (h i); constructor <;> linarith [this.1, this.2] · rw [abs_le]; have := h i; constructor <;> linarith [this.1, this.2]
    Causalean.Stat.Nonparametric.supBall_eq_pi · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:46
  • measurableSet_supBall lemma — A closed sup-norm ball (an axis-aligned cube, or box) is a measurable set.
    hypotheses
    d :
    ℕ
    x0 :
    Fin d → ℝ
    r :
    ℝ
    conclusion
    MeasurableSet (supBall x0 r)
    Proof (Lean source)
    lemma measurableSet_supBall {d : ℕ} (x0 : Fin d → ℝ) (r : ℝ) : MeasurableSet (supBall x0 r) := by rw [supBall_eq_pi]; exact MeasurableSet.univ_pi (fun _ => measurableSet_Icc)
    Causalean.Stat.Nonparametric.measurableSet_supBall · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:63
  • mem_supBall_self lemma — A closed sup-norm ball (axis-aligned cube) of nonnegative half-width contains its own centre.
    hypotheses
    d :
    ℕ
    x0 :
    Fin d → ℝ
    r :
    ℝ
    hr :
    0 ≤ r
    conclusion
    x0 ∈ supBall x0 r
    Proof (Lean source)
    lemma mem_supBall_self {d : ℕ} (x0 : Fin d → ℝ) {r : ℝ} (hr : 0 ≤ r) : x0 ∈ supBall x0 r := by intro i; simp only [sub_self, abs_zero]; exact hr
    Causalean.Stat.Nonparametric.mem_supBall_self · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:68
  • mem_cube lemma — Membership in an axis-aligned box: a point lies in it exactly when each of its coordinates lies between a and b.
    hypotheses
    ι :
    Type*
    a b :
    ℝ
    x :
    ι → ℝ
    conclusion
    x ∈ Set.univ.pi (fun _ : ι => Icc a b) ↔ ∀ i, a ≤ x i ∧ x i ≤ b
    Proof (Lean source)
    lemma mem_cube {ι : Type*} {a b : ℝ} {x : ι → ℝ} : x ∈ Set.univ.pi (fun _ : ι => Icc a b) ↔ ∀ i, a ≤ x i ∧ x i ≤ b := by simp only [Set.mem_univ_pi, Set.mem_Icc]
    Causalean.Stat.Nonparametric.mem_cube · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:84
  • isCompact_cube lemma — An axis-aligned box over a finite index type is compact: it is a finite product of closed bounded intervals.
    hypotheses
    ι :
    Type*
    Finite ι
    a b :
    ℝ
    conclusion
    IsCompact (Set.univ.pi (fun _ : ι => Icc a b))
    Proof (Lean source)
    lemma isCompact_cube {ι : Type*} [Finite ι] (a b : ℝ) : IsCompact (Set.univ.pi (fun _ : ι => Icc a b)) := by letI := ofFinite ι exact isCompact_univ_pi (fun _ => isCompact_Icc)
    Causalean.Stat.Nonparametric.isCompact_cube · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Defs.lean:90
Kernel 1 core · 3 supporting Milestone 1 of the Tsybakov interpolation primitive: a bounded, compactly supported product kernel K on [-1,1]^d with total mass 1 and vanishing moments up to order m = ⌈γ⌉₊ - 1. ★ exists_moment_cancelling_kernel_1d

Moment-cancelling product kernel (Milestone 1)

Milestone 1 of the Tsybakov interpolation primitive: a bounded, compactly supported product kernel K on [-1,1]^d with total mass 1 and vanishing moments up to order m = ⌈γ⌉₊ - 1.

* exists_moment_cancelling_kernel_1d — the 1-D building block: a continuous, [-1,1]-supported kernel k with ∫ k = 1 and ∫ uʲ k(u) du = 0 for 1 ≤ j ≤ m. Obtained by the standard Vandermonde/Gram moment solve: take a fixed positive continuous weight vanishing at ±1 and multiply by a degree-m polynomial whose coefficients solve the nonsingular moment (Gram) system. * prodKernel_abs_le — the tensorized kernel is bounded by B ^ d when k is bounded by B.

The multivariate mass-1 / vanishing-moment consequences of tensorization are derived at the point of use in HolderInterpolation.lean (Fubini over the product Lebesgue measure), so this file only exposes the 1-D solve and the pointwise bound.

theorem exists_moment_cancelling_kernel_1d reviewed
Causalean.Stat.Nonparametric

For any prescribed finite order m, a compactly supported one-dimensional kernel can be chosen to have unit total mass while cancelling every polynomial moment through that order.

Formal statement
hypotheses
m :
ℕ
conclusion
∃ k : ℝ → ℝ,
Continuous k ∧
(∀ u : ℝ, 1 < |u| → k u = 0) ∧
(∫ u in Icc (-1 : ℝ) 1, k u) = 1 ∧
(∀ j : ℕ, 1 ≤ j → j ≤ m → (∫ u in Icc (-1 : ℝ) 1, u ^ j * k u) = 0)
Proof (Lean source)
theorem exists_moment_cancelling_kernel_1d (m : ℕ) : ∃ k : ℝ → ℝ, Continuous k ∧ (∀ u : ℝ, 1 < |u| → k u = 0) ∧ (∫ u in Icc (-1 : ℝ) 1, k u) = 1 ∧ (∀ j : ℕ, 1 ≤ j → j ≤ m → (∫ u in Icc (-1 : ℝ) 1, u ^ j * k u) = 0) := by -- Solve the Gram system `G c = e₀` by injectivity ⟹ surjectivity of a -- finite-dimensional endomorphism. have hsurj : Surjective ((hpkGram m).mulVecLin) := by rw [← LinearMap.injective_iff_surjective, ← LinearMap.ker_eq_bot, Matrix.ker_mulVecLin_eq_bot_iff] exact fun v hv => hpkInjective m v hv obtain ⟨c, hc⟩ := hsurj (single 0 1) rw [Matrix.mulVecLin_apply] at hc -- The moment integrals of `k = max(1-u²,0) · p(u)` over `[-1,1]` equal the Gram rows. have hmom : ∀ J : Fin (m + 1), (∫ u in Icc (-1 : ℝ) 1, u ^ (J : ℕ) * (max (1 - u ^ 2) 0 * hpkPoly m c u)) = (hpkGram m).mulVec c J := by intro J rw [MeasureTheory.setIntegral_congr_fun measurableSet_Icc (f := fun u => u ^ (J : ℕ) * (max (1 - u ^ 2) 0 * hpkPoly m c u)) (g := fun u => u ^ (J : ℕ) * ((1 - u ^ 2) * hpkPoly m c u)) (fun u hu => by dsimp only rw [max_eq_left (by nlinarith [hu.1, hu.2] : (0 : ℝ) ≤ 1 - u ^ 2)])] exact hpkExpand m c J refine ⟨fun u => max (1 - u ^ 2) 0 * hpkPoly m c u, ?_, ?_, ?_, ?_⟩ · exact ((continuous_const.sub (continuous_pow 2)).max continuous_const).mul (hpkPoly_continuous m c) · intro u hu have h1 : (1 : ℝ) < u ^ 2 := by nlinarith [hu, sq_abs u, abs_nonneg u] dsimp only rw [max_eq_right (by linarith : (1 : ℝ) - u ^ 2 ≤ 0), zero_mul] · have h0 := hmom 0 rw [hc, Pi.single_eq_same] at h0 simp only [Fin.val_zero, pow_zero, one_mul] at h0 simpa using h0 · intro j hj1 hjm have hJ : j < m + 1 := by omega have h0 := hmom ⟨j, hJ⟩ rw [hc, Pi.single_apply, if_neg (by intro h; rw [Fin.ext_iff] at h; simp at h; omega)] at h0 simpa using h0
Causalean.Stat.Nonparametric.exists_moment_cancelling_kernel_1d · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Kernel.lean:158
3 supporting declarations (lemmas, instances)
  • prodKernel_abs_le theorem — A product kernel is uniformly bounded by the coordinatewise bound raised to the dimension, whenever its one-dimensional factor has that bound.
    hypotheses
    d :
    ℕ
    k :
    ℝ → ℝ
    B :
    ℝ
    hB :
    ∀ u, |k u| ≤ B
    u :
    Fin d → ℝ
    conclusion
    |prodKernel k d u| ≤ B ^ d
    Proof (Lean source)
    theorem prodKernel_abs_le {d : ℕ} {k : ℝ → ℝ} {B : ℝ} (hB : ∀ u, |k u| ≤ B) (u : Fin d → ℝ) : |prodKernel k d u| ≤ B ^ d := by unfold prodKernel rw [Finset.abs_prod] calc ∏ i : Fin d, |k (u i)| ≤ ∏ _i : Fin d, B := Finset.prod_le_prod (fun i _ => abs_nonneg _) (fun i _ => hB (u i)) _ = B ^ d := by rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin]
    Causalean.Stat.Nonparametric.prodKernel_abs_le · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Kernel.lean:211
  • prodKernel_integral theorem — The total mass of a product kernel factorizes into the product of the one-dimensional masses, so a unit-mass factor yields a unit-mass multivariate kernel.
    hypotheses
    d :
    ℕ
    k :
    ℝ → ℝ
    conclusion
    ∫ u, prodKernel k d u = (∫ t, k t) ^ d
    Proof (Lean source)
    theorem prodKernel_integral {d : ℕ} (k : ℝ → ℝ) : ∫ u, prodKernel k d u = (∫ t, k t) ^ d := by unfold prodKernel rw [MeasureTheory.integral_fintype_prod_volume_eq_prod (fun _ : Fin d => k)] rw [Finset.prod_const, Finset.card_univ, Fintype.card_fin]
    Causalean.Stat.Nonparametric.prodKernel_integral · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Kernel.lean:224
  • prodKernel_moment theorem — Each polynomial moment of a product kernel factorizes into the corresponding one-dimensional moments, allowing any cancelled coordinate moment to cancel the entire multivariate moment.
    hypotheses
    d :
    ℕ
    k :
    ℝ → ℝ
    ν :
    Fin d → ℕ
    conclusion
    (∫ u, (∏ i, u i ^ ν i) * prodKernel k d u) = ∏ i, ∫ t, t ^ ν i * k t
    Proof (Lean source)
    theorem prodKernel_moment {d : ℕ} (k : ℝ → ℝ) (ν : Fin d → ℕ) : (∫ u, (∏ i, u i ^ ν i) * prodKernel k d u) = ∏ i, ∫ t, t ^ ν i * k t := by unfold prodKernel have hfac : (fun u : Fin d → ℝ => (∏ i, u i ^ ν i) * ∏ i, k (u i)) = fun u : Fin d → ℝ => ∏ i, (u i ^ ν i * k (u i)) := by funext u; rw [← Finset.prod_mul_distrib] rw [hfac] rw [MeasureTheory.integral_fintype_prod_volume_eq_prod (fun i : Fin d => fun t => t ^ ν i * k t)]
    Causalean.Stat.Nonparametric.prodKernel_moment · Causalean/Stat/Nonparametric/Approximation/HolderInterpolation/Kernel.lean:232