Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
This package supplies the normalized cosine basis on the unit interval, its finite uniform-measure projection, an even Jackson approximant, and the constant-five Hölder L² error bound.
Definitions 10 core · 0 supporting Research-independent definitions for uniform design on [0,1].
Normalized cosine projection on the unit interval
Research-independent definitions for uniform design on [0,1]. Real functions are
defined on the real line, but all regularity assumptions below concern only the
closed unit interval. The extended norm uses a nonnegative integral, preserving
infinite values; the real norm is used only after integrability has been established.
The rank counts the constant mode: rank one means projection onto constants.
def uniformMeasure reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
Uniform probability on the unit interval is Lebesgue measure restricted to the closed interval from zero to one.
def cosineBasis reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The normalized cosine mode with index at position is one for the zero mode and square root of two times cosine of π times index times position otherwise.
def cosineCoefficient reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The coefficient of a function in mode is its uniform integral against that normalized mode.
Definition (Lean source)
parameters
f :
ℝ → ℝ
j :
ℕ
def
cosineCoefficient f j :
ℝ
given by
∫ x, f x * cosineBasis j x ∂uniformMeasure
def cosinePolynomial reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The cosine polynomial at rank with coefficients evaluated at position sums the modes with indices strictly below the rank.
Definition (Lean source)
parameters
k :
ℕ
a :
ℕ → ℝ
x :
ℝ
def
cosinePolynomial k a x :
ℝ
given by
∑ j ∈ range k, a j * cosineBasis j x
def cosineProjection reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The finite cosine projection of a function, at rank and position, uses its uniform cosine coefficients.
Definition (Lean source)
parameters
k :
ℕ
f :
ℝ → ℝ
x :
ℝ
def
cosineProjection k f x :
ℝ
given by
cosinePolynomial k (cosineCoefficient f) x
def InCosineSpan reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The cosine span condition for a function at rank means it equals a normalized cosine polynomial everywhere on the unit interval.
Definition (Lean source)
parameters
k :
ℕ
p :
ℝ → ℝ
def
InCosineSpan k p :
Prop
given by
∃ a : ℕ → ℝ, ∀ x ∈ Icc (0 : ℝ) 1, p x = cosinePolynomial k a x
def l2Norm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The real uniform L² norm of a function is the square root of the integral of its squared absolute value. For nonintegrable functions the real integral has Lean's default value; use the extended norm in that case.
Definition (Lean source)
def extendedL2Norm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The extended uniform L² norm of a function is the square root of the nonnegative integral of its squared absolute value.
Definition (Lean source)
parameters
g :
ℝ → ℝ
def
extendedL2Norm g :
ℝ≥0∞
given by
(∫⁻ x, ofReal (|g x| ^ 2) ∂uniformMeasure) ^ (1 / 2 : ℝ)
def holderSeminorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The extended Hölder seminorm of a function, with exponent, is the supremum of its absolute increments divided by distance to that exponent, over distinct points in the closed unit interval.
def HasHolderBound reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
A Hölder bound for a function, exponent, and constant is the increment inequality for every pair in the unit interval.
Definition (Lean source)
parameters
f :
ℝ → ℝ
γ H :
ℝ
x ∈ Set.Icc (0 : ℝ) 1 :
z ∈ Set.Icc (0 : ℝ) 1 :
def
HasHolderBound f γ H :
Prop
given by
|f x - f z| ≤ H * |x - z| ^ γ
JacksonError 2 core · 1 supporting Define the Jackson approximant and isolate its analytic error estimate from finite cosine expansion. ★ jacksonApproximant_error
Continuity and uniform error of the even Jackson convolution
Define the Jackson approximant and isolate its analytic error estimate from finite cosine expansion. This module depends only on the closed fold and moment layers; its proofs need no projection, orthogonality, or convolution-window expansion.
def jacksonApproximant reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The Jackson cosine approximant of a target, at order and position, convolves its even angular extension with the unit-mass order-four Jackson kernel.
theorem jacksonApproximant_error reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
For an exponent between zero and one, a nonnegative Hölder bound, a continuous target, and a positive order, the Jackson uniform error is bounded by the Hölder constant times (2/K)^γ, at every unit-interval point.
Formal statement
hypotheses
K :
ℕ
f :
ℝ → ℝ
γ H x :
ℝ
hK :
0 < K
hf :
ContinuousOn f (Icc (0 : ℝ) 1)
hγ :
0 < γ
hγ1 :
γ ≤ 1
hH :
0 ≤ H
hholder :
HasHolderBound f γ H
hx :
x ∈ Icc (0 : ℝ) 1
conclusion
|f x - jacksonApproximant K f x| ≤ H * (2 / (K : ℝ)) ^ γ
Proof (Lean source)
theorem jacksonApproximant_error {K : ℕ} {f : ℝ → ℝ} {γ H x : ℝ}
(hK : 0 < K) (hf : ContinuousOn f (Icc (0 : ℝ) 1))
(hγ : 0 < γ) (hγ1 : γ ≤ 1) (hH : 0 ≤ H) (hholder : HasHolderBound f γ H)
(hx : x ∈ Icc (0 : ℝ) 1) :
|f x - jacksonApproximant K f x| ≤ H * (2 / (K : ℝ)) ^ γ := by
have hext := continuous_evenExtension hf
have hkernel := continuous_jackson K
have hconv : Continuous (fun t => evenExtension f (pi * x - t) *
jackson K t) := by fun_prop
have hinc : Continuous (fun t => (f x - evenExtension f (pi * x - t)) *
jackson K t) := by fun_prop
have hpow : Continuous (fun t : ℝ => (|t| / pi) ^ γ) :=
(continuous_abs.div_const pi).rpow_const (fun _ => inr hγ.le)
have hbound : Continuous (fun t => H * ((|t| / pi) ^ γ * jackson K t)) :=
continuous_const.mul (hpow.mul hkernel)
have herr : f x - jacksonApproximant K f x =
∫ t in Icc (-pi) pi,
(f x - evenExtension f (pi * x - t)) * jackson K t := by
simp_rw [sub_mul]
rw [integral_sub ((integrableOn_jackson K).const_mul (f x))
(hconv.continuousOn.integrableOn_compact isCompact_Icc),
integral_const_mul, jackson_integral_eq_one K hK, mul_one]
rfl
rw [herr]
calc
_ ≤ ∫ t in Icc (-pi) pi,
|(f x - evenExtension f (pi * x - t)) * jackson K t| :=
abs_integral_le_integral_abs
_ ≤ ∫ t in Icc (-pi) pi,
H * ((|t| / pi) ^ γ * jackson K t) := by
apply setIntegral_mono_on
(hinc.abs.continuousOn.integrableOn_compact isCompact_Icc)
(hbound.continuousOn.integrableOn_compact isCompact_Icc) measurableSet_Icc
intro t ht
have hh := evenExtension_holder hγ hH hholder (pi * x) (pi * x - t)
rw [evenExtension_pi_mul f hx, sub_sub_cancel] at hh
rw [abs_mul, abs_of_nonneg (jackson_nonneg K hK t)]
exact (mul_le_mul_of_nonneg_right hh (jackson_nonneg K hK t)).trans_eq
(mul_assoc _ _ _)
_ = H * ∫ t in Icc (-pi) pi,
(|t| / pi) ^ γ * jackson K t := integral_const_mul _ _
_ ≤ _ := mul_le_mul_of_nonneg_left (jackson_holder_moment hK hγ hγ1) hH
1 supporting declaration (lemmas, instances)
-
continuous_jacksonApproximanttheorem — A target continuous on the closed interval has continuous Jackson approximant at every order.hypothesesconclusionContinuous (jacksonApproximant K f)Proof (Lean source)
@[fun_prop] theorem continuous_jacksonApproximant {K : ℕ} {f : ℝ → ℝ} (hf : ContinuousOn f (Icc (0 : ℝ) 1)) : Continuous (jacksonApproximant K f) := by unfold jacksonApproximant apply continuous_parametric_integral_of_continuous (s := Icc (-pi) pi) (hs := isCompact_Icc) have hext := continuous_evenExtension hf have hkernel := continuous_jackson K fun_prop
Approximation 1 core · 1 supporting Use convolution of the even periodic extension against the existing Jackson kernel, defined in JacksonError. ★ exists_cosine_approximant
The even Jackson approximant in the cosine span
Use convolution of the even periodic extension against the existing Jackson kernel, defined in JacksonError. Finite-degree membership and uniform Hölder error are separate obligations: no spectral approximation result is assumed in the definition.
theorem exists_cosine_approximant reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
For a positive rank, a continuous target, an exponent between zero and one, and a nonnegative Hölder bound, there is a continuous rank-k cosine approximant with uniform error at most five times the Hölder constant times k⁻γ.
Formal statement
hypotheses
k :
ℕ
f :
ℝ → ℝ
γ H :
ℝ
hk :
1 ≤ k
hf :
ContinuousOn f (Icc (0 : ℝ) 1)
hγ :
0 < γ
hγ1 :
γ ≤ 1
hH :
0 ≤ H
hholder :
HasHolderBound f γ H
conclusion
∃ p : ℝ → ℝ,
ContinuousOn p (Icc (0 : ℝ) 1)
InCosineSpan k p
conclusion 1
x ∈ Set.Icc (0 : ℝ) 1 :
|f x - p x| ≤ 5 * H * (k : ℝ) ^ (-γ)
Proof (Lean source)
theorem exists_cosine_approximant {k : ℕ} {f : ℝ → ℝ} {γ H : ℝ}
(hk : 1 ≤ k) (hf : ContinuousOn f (Icc (0 : ℝ) 1))
(hγ : 0 < γ) (hγ1 : γ ≤ 1) (hH : 0 ≤ H) (hholder : HasHolderBound f γ H) :
∃ p : ℝ → ℝ, ContinuousOn p (Icc (0 : ℝ) 1) ∧ InCosineSpan k p ∧
∀ x ∈ Icc (0 : ℝ) 1, |f x - p x| ≤ 5 * H * (k : ℝ) ^ (-γ) := by
let K : ℕ := (k + 1) / 2
have hK : 0 < K := (matchedOrder_bounds hk).1
refine ⟨jacksonApproximant K f, (continuous_jacksonApproximant hf).continuousOn,
inCosineSpan_mono (by have := (matchedOrder_bounds hk).2; omega)
(jacksonApproximant_mem_span hK hf), ?_⟩
intro x hx
calc
_ ≤ H * (2 / (K : ℝ)) ^ γ :=
jacksonApproximant_error hK hf hγ hγ1 hH hholder hx
_ ≤ H * (5 * (k : ℝ) ^ (-γ)) :=
mul_le_mul_of_nonneg_left (matchedOrder_constant_five hk hγ hγ1) hH
_ = _ := by ring
1 supporting declaration (lemmas, instances)
-
jacksonApproximant_mem_spantheorem — At a positive order, a target continuous on the closed interval has Jackson approximant in the cosine span through degree twice the predecessor of its order.hypothesesconclusionInCosineSpan (2 * (K - 1) + 1) (jacksonApproximant K f)Proof (Lean source)
theorem jacksonApproximant_mem_span {K : ℕ} {f : ℝ → ℝ} (hK : 0 < K) (hf : ContinuousOn f (Icc (0 : ℝ) 1)) : InCosineSpan (2 * (K - 1) + 1) (jacksonApproximant K f) := by classical obtain ⟨a, ha⟩ := even_trigPoly_cosine (jackson_isTrigPolyLE K hK) (jackson_even K) let b : ℕ → ℝ := fun j => a j * ∫ t in Icc (-pi) pi, evenExtension f t * cos ((j : ℝ) * t) refine ⟨fun j => if j = 0 then b j else b j / sqrt 2, ?_⟩ intro x hx change angularConvolution (evenExtension f) (jackson K) (pi * x) = _ rw [angularConvolution_cosine_expansion (continuous_evenExtension hf) (evenExtension_even f) (evenExtension_periodic f) a ha] unfold cosinePolynomial apply Finset.sum_congr rfl intro j hj change b j * cos ((j : ℝ) * (pi * x)) = _ by_cases hzero : j = 0 · subst j simp [cosineBasis] · simp only [cosineBasis, hzero, if_false] rw [show (j : ℝ) * (pi * x) = pi * (j : ℝ) * x by ring] have hsqrt : sqrt 2 ≠ 0 := ne_of_gt (Real.sqrt_pos.2 (by norm_num)) field_simp
Convolution 2 core · 2 supporting Separate the change of integration window, removal of sine modes, and explicit convolution coefficients before attempting Jackson span membership. ★ angularConvolution_cosine_expansion
Finite cosine expansion of even periodic convolution
Separate the change of integration window, removal of sine modes, and explicit convolution coefficients before attempting Jackson span membership. These are generic angular statements independent of the target's Hölder regularity and of the numerical Jackson moment bounds.
def angularConvolution reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
Angular convolution of a target and kernel at an angle integrates their translated product over the principal period.
theorem angularConvolution_cosine_expansion reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
A continuous even periodic target convolved with a finite cosine kernel has the explicit cosine expansion obtained by multiplying kernel coefficients by target cosine integrals, at every angle.
Formal statement
hypotheses
Proof (Lean source)
theorem angularConvolution_cosine_expansion {n : ℕ} {g h : ℝ → ℝ}
(hg : Continuous g) (hgeven : Even g)
(hgper : Periodic g (2 * pi)) (a : ℕ → ℝ)
(hexp : ∀ t : ℝ,
h t = ∑ j ∈ range (n + 1), a j * cos ((j : ℝ) * t)) (θ : ℝ) :
angularConvolution g h θ =
∑ j ∈ range (n + 1),
(a j * ∫ t in Icc (-pi) pi, g t * cos ((j : ℝ) * t)) *
cos ((j : ℝ) * θ) := by
classical
have hh : Continuous h := by
have heq : h = fun t => ∑ j ∈ range (n + 1),
a j * cos ((j : ℝ) * t) := funext hexp
rw [heq]
fun_prop
have hhper : Periodic h (2 * pi) := by
intro t
rw [hexp, hexp]
apply Finset.sum_congr rfl
intro j hj
rw [mul_add, Real.cos_add_nat_mul_two_pi]
rw [angularConvolution_reverse hgper hhper θ]
have hle : -pi ≤ pi := by linarith [Real.pi_pos]
simp only [integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hle]
have hsine (j : ℕ) :
(∫ t in -Real.pi..Real.pi, g t * sin ((j : ℝ) * t)) = 0 := by
have href := intervalIntegral.integral_comp_neg
(a := -pi) (b := pi)
(fun t => g t * sin ((j : ℝ) * t))
simp only [show ∀ t, g (-t) = g t from hgeven, mul_neg, Real.sin_neg, mul_neg,
intervalIntegral.integral_neg, neg_neg] at href
linarith
have hfun : (fun t => g t * h (θ - t)) =
(fun t => ∑ j ∈ range (n + 1),
(a j * (g t * cos ((j : ℝ) * t)) * cos ((j : ℝ) * θ) +
a j * (g t * sin ((j : ℝ) * t)) * sin ((j : ℝ) * θ))) := by
funext t
rw [hexp, Finset.mul_sum]
apply Finset.sum_congr rfl
intro j hj
rw [mul_sub, Real.cos_sub]
ring
rw [hfun, intervalIntegral.integral_finsetSum]
· apply Finset.sum_congr rfl
intro j hj
rw [intervalIntegral.integral_add]
· simp only [intervalIntegral.integral_mul_const,
intervalIntegral.integral_const_mul, hsine, mul_zero, zero_mul, add_zero]
· exact (show Continuous (fun t =>
a j * (g t * cos ((j : ℝ) * t)) * cos ((j : ℝ) * θ)) by
fun_prop).intervalIntegrable _ _
· exact (show Continuous (fun t =>
a j * (g t * sin ((j : ℝ) * t)) * sin ((j : ℝ) * θ)) by
fun_prop).intervalIntegrable _ _
· intro j hj
exact (show Continuous (fun t =>
a j * (g t * cos ((j : ℝ) * t)) * cos ((j : ℝ) * θ) +
a j * (g t * sin ((j : ℝ) * t)) * sin ((j : ℝ) * θ)) by
fun_prop).intervalIntegrable _ _
2 supporting declarations (lemmas, instances)
-
angularConvolution_reversetheorem — Two periodic functions satisfy the reversed angular convolution formula at every angle.hypothesesconclusionProof (Lean source)
theorem angularConvolution_reverse {g h : ℝ → ℝ} (hgper : Periodic g (2 * pi)) (hhper : Periodic h (2 * pi)) (θ : ℝ) : angularConvolution g h θ = ∫ t in Icc (-pi) pi, g t * h (θ - t) := by have hle : -pi ≤ pi := by linarith [Real.pi_pos] simp only [angularConvolution, integral_Icc_eq_integral_Ioc, ← intervalIntegral.integral_of_le hle] let f : ℝ → ℝ := fun t => g t * h (θ - t) have hfper : Periodic f (2 * pi) := by intro t dsimp [f] rw [hgper t] have ht : θ - (t + 2 * pi) = (θ - t) - 2 * pi := by ring rw [ht, hhper.sub_eq] have hcomp : (fun t => g (θ - t) * h t) = (fun t => f (θ - t)) := by funext t simp [f] rw [hcomp, intervalIntegral.integral_comp_sub_left] have hp := hfper.intervalIntegral_add_eq (θ - pi) (-pi) convert hp using 1 <;> congr 1 <;> ring -
even_trigPoly_cosinetheorem — An even real trigonometric polynomial has a finite expansion using only cosine modes, with the same degree bound.hypothesesProof (Lean source)
theorem even_trigPoly_cosine {n : ℕ} {h : ℝ → ℝ} (hh : IsTrigPolyLE n h) (heven : Even h) : ∃ a : ℕ → ℝ, ∀ t : ℝ, h t = ∑ j ∈ range (n + 1), a j * cos ((j : ℝ) * t) := by classical rcases hh with ⟨a, b, hh⟩ refine ⟨a, fun t => ?_⟩ have ht := hh t have hnt := hh (-t) rw [heven t] at hnt simp only [mul_neg, Real.cos_neg, Real.sin_neg, mul_neg] at hnt have havg : h t + h t = ∑ j ∈ range (n + 1), 2 * (a j * cos ((j : ℝ) * t)) := by nth_rw 1 [ht] rw [hnt, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro j hj ring rw [← Finset.mul_sum] at havg linarith
Fold 3 core · 10 supporting The fold arccos(cos(t))/π maps the line continuously into [0,1], agrees with t/π on [0,π], and is even and 2π-periodic. ★ fold_lipschitz
The even periodic extension of a unit-interval function
The fold arccos(cos(t))/π maps the line continuously into [0,1], agrees
with t/π on [0,π], and is even and 2π-periodic. Its global Lipschitz bound
is the independent geometric obligation behind Hölder extension; differentiating
arccos at ±1 would incorrectly exclude the endpoints.
def fold reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The folded unit-interval position of an angle is its cosine's principal arccosine divided by π.
def evenExtension reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The even periodic extension of an interval function at an angle evaluates that function at the folded position.
Definition (Lean source)
theorem fold_lipschitz reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
Folded positions at two angles have distance at most angular distance divided by π.
Proof (Lean source)
theorem fold_lipschitz (s t : ℝ) : |fold s - fold t| ≤ |s - t| / pi := by
have h : |arccos (cos s) - arccos (cos t)| ≤ |s - t| := by
rw [abs_le]
have hst := arccos_cos_le_add s t
have hts := arccos_cos_le_add t s
rw [abs_sub_comm t s] at hts
constructor <;> linarith
simpa only [fold, ← sub_div, abs_div, abs_of_pos Real.pi_pos] using
(div_le_div_of_nonneg_right h Real.pi_pos.le)
10 supporting declarations (lemmas, instances)
-
fold_memtheorem — The folded position at every angle lies in the unit interval. -
continuous_foldtheorem — The angular fold is continuous.conclusionProof (Lean source)
@[fun_prop] theorem continuous_fold : Continuous fold := by exact (Real.continuous_arccos.comp Real.continuous_cos).div_const pi -
fold_pi_multheorem — The fold recovers each unit-interval point after scaling by π, for a point in that interval.Proof (Lean source)
theorem fold_pi_mul {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) : fold (pi * x) = x := by unfold fold rw [Real.arccos_cos (mul_nonneg Real.pi_pos.le hx.1) (by nlinarith [Real.pi_pos, hx.2])] exact mul_div_cancel_left₀ x Real.pi_ne_zero -
continuous_evenExtensiontheorem — A function continuous on the closed unit interval has continuous even periodic extension on the real line.Proof (Lean source)
@[fun_prop] theorem continuous_evenExtension {f : ℝ → ℝ} (hf : ContinuousOn f (Icc (0 : ℝ) 1)) : Continuous (evenExtension f) := by exact hf.comp_continuous continuous_fold fold_mem -
evenExtension_eventheorem — The folded extension of an interval function is even.Proof (Lean source)
theorem evenExtension_even (f : ℝ → ℝ) : Even (evenExtension f) := by intro t exact congrArg f (fold_even t) -
evenExtension_periodictheorem — The folded extension of an interval function has period 2π.Proof (Lean source)
theorem evenExtension_periodic (f : ℝ → ℝ) : Periodic (evenExtension f) (2 * pi) := by intro t exact congrArg f (fold_periodic t) -
evenExtension_pi_multheorem — The even extension recovers the original function at a π-scaled unit-interval point, for an interval function.Proof (Lean source)
theorem evenExtension_pi_mul (f : ℝ → ℝ) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) : evenExtension f (pi * x) = f x := by simp only [evenExtension, fold_pi_mul hx] -
evenExtension_holdertheorem — A unit-interval Hölder increment bound at a positive exponent with a nonnegative constant gives the angular increment bound, with distance divided by π, for its even extension.hypothesesf :ℝ → ℝγ H :ℝhγ :0 < γhH :0 ≤ Hs t :ℝconclusionProof (Lean source)
theorem evenExtension_holder {f : ℝ → ℝ} {γ H : ℝ} (hγ : 0 < γ) (hH : 0 ≤ H) (hf : ∀ x ∈ Icc (0 : ℝ) 1, ∀ z ∈ Icc (0 : ℝ) 1, |f x - f z| ≤ H * |x - z| ^ γ) (s t : ℝ) : |evenExtension f s - evenExtension f t| ≤ H * (|s - t| / pi) ^ γ := by exact (hf (fold s) (fold_mem s) (fold t) (fold_mem t)).trans (mul_le_mul_of_nonneg_left (Real.rpow_le_rpow (abs_nonneg _) (fold_lipschitz s t) hγ.le) hH)
Main 1 core · 1 supporting The real finite-bound and extended-seminorm interfaces establish the constant-five uniform L² approximation rate for finite normalized cosine projections. ★ cosineProjection_error_le_seminorm
Constant-five Hölder approximation by the normalized cosine projection
The real finite-bound and extended-seminorm interfaces establish the constant-five uniform L² approximation rate for finite normalized cosine projections. The infinite-seminorm case is retained explicitly, so the public result has exactly the interval continuity, exponent, and rank assumptions required for nonparametric series approximation.
theorem cosineProjection_error_le_seminorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
A continuous real function on the unit interval, an exponent between zero and one, and a positive rank give extended L² projection error at most five times the extended Hölder seminorm times k⁻γ, including infinite seminorm.
Formal statement
hypotheses
conclusion
extendedL2Norm (fun x => f x - cosineProjection k f x)
≤ 5 * holderSeminorm f γ * ofReal ((k : ℝ) ^ (-γ))
Proof (Lean source)
theorem cosineProjection_error_le_seminorm {f : ℝ → ℝ} {γ : ℝ} {k : ℕ}
(hf : ContinuousOn f (Icc (0 : ℝ) 1))
(hγ : 0 < γ) (hγ1 : γ ≤ 1) (hk : 1 ≤ k) :
extendedL2Norm (fun x => f x - cosineProjection k f x) ≤
5 * holderSeminorm f γ * ofReal ((k : ℝ) ^ (-γ)) := by
by_cases htop : holderSeminorm f γ = ⊤
· exact extended_bound_of_seminorm_top hk htop
· have hres : ContinuousOn (fun x => f x - cosineProjection k f x)
(Icc (0 : ℝ) 1) :=
hf.sub (continuous_cosinePolynomial k (cosineCoefficient f)).continuousOn
rw [extendedL2Norm_eq_ofReal hres]
have hreal := cosineProjection_error_le hf hγ hγ1 hk
(ENNReal.toReal_nonneg : 0 ≤ (holderSeminorm f γ).toReal)
(hasHolderBound_seminorm hγ htop)
calc
_ ≤ ofReal (5 * (holderSeminorm f γ).toReal * (k : ℝ) ^ (-γ)) :=
ENNReal.ofReal_le_ofReal hreal
_ = _ := by
rw [ENNReal.ofReal_mul (by positivity), ENNReal.ofReal_mul (by norm_num),
ENNReal.ofReal_toReal htop]
norm_num
1 supporting declaration (lemmas, instances)
-
cosineProjection_error_letheorem — A continuous real function on the unit interval, an exponent between zero and one, a positive rank, and a nonnegative Hölder constant satisfying its increment bound give L² cosine projection error at most five times that constant times k⁻γ.hypothesesf :ℝ → ℝγ H :ℝk :ℕhf :ContinuousOn f (Icc (0 : ℝ) 1)hγ :0 < γhγ1 :γ ≤ 1hk :1 ≤ khH :0 ≤ Hhholder :HasHolderBound f γ Hconclusionl2Norm (fun x => f x - cosineProjection k f x) ≤ 5 * H * (k : ℝ) ^ (-γ)Proof (Lean source)
theorem cosineProjection_error_le {f : ℝ → ℝ} {γ H : ℝ} {k : ℕ} (hf : ContinuousOn f (Icc (0 : ℝ) 1)) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hk : 1 ≤ k) (hH : 0 ≤ H) (hholder : HasHolderBound f γ H) : l2Norm (fun x => f x - cosineProjection k f x) ≤ 5 * H * (k : ℝ) ^ (-γ) := by obtain ⟨p, hp, hspan, herr⟩ := exists_cosine_approximant hk hf hγ hγ1 hH hholder apply (cosineProjection_bestApproximation hf hspan).trans exact l2Norm_le_of_abs_le (hf.sub hp) (by positivity) herr
Moments 1 core · 5 supporting Reuse Causalean's unit-mass order-four kernel and exact mass. ★ jackson_holder_moment
Jackson moments sufficient for constant five
Reuse Causalean's unit-mass order-four kernel and exact mass. The existing public 64/K² bound loses too much when translated to rank. Instead the sine chord bound gives the raw weighted estimate, whose normalization is at most 3π²/(2K²). We retain the convenient weaker bound (2π/K)². Jensen at exponent γ/2 then gives the unit-coordinate γ-moment at most (2/K)^γ. For K=(k+1)/2, the rank factor is at most 4^γ ≤ 4 ≤ 5, including k=1.
Reference for conventions: Cambridge Part III Approximation Theory, Lecture 9 (2005), Definitions 9.3 and 9.5, Lemma 9.6, Theorem 9.8: https://www.damtp.cam.ac.uk/user/na/PartIIIat/b09.pdf . The source supplies the classical construction, not the explicit constant claimed here. All numerical bounds below remain formal proof obligations.
theorem jackson_holder_moment reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
A positive order and an exponent between zero and one give a Jackson Hölder moment in unit coordinates at most (2/K)^γ.
Formal statement
Proof (Lean source)
theorem jackson_holder_moment {K : ℕ} {γ : ℝ}
(hK : 0 < K) (hγ : 0 < γ) (hγ1 : γ ≤ 1) :
(∫ t in Icc (-pi) pi, (|t| / pi) ^ γ * jackson K t) ≤
(2 / (K : ℝ)) ^ γ := by
let μ : Measure ℝ := volume.restrict (Icc (-pi) pi)
let w : ℝ → ℝ≥0∞ := fun t => ofReal (jackson K t)
let ν : Measure ℝ := μ.withDensity w
have hw : Measurable w := (measurable_jackson K).ennreal_ofReal
have hwtop : ∀ᵐ t ∂μ, w t < ∞ := Filter.Eventually.of_forall
(fun t => ENNReal.ofReal_lt_top)
have hnonneg : ∀ t, 0 ≤ jackson K t := jackson_nonneg K hK
have hbridge (f : ℝ → ℝ) : (∫ t, f t ∂ν) =
∫ t in Icc (-pi) pi, f t * jackson K t := by
rw [integral_withDensity_eq_integral_toReal_smul hw hwtop]
simp only [w, ENNReal.toReal_ofReal (hnonneg _), smul_eq_mul, mul_comm]
rfl
have hν : ν univ = 1 := by
change μ.withDensity w univ = 1
rw [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ]
change (∫⁻ t, ofReal (jackson K t) ∂μ) = 1
rw [← ofReal_integral_eq_lintegral_ofReal (integrableOn_jackson K)
(Filter.Eventually.of_forall hnonneg), jackson_integral_eq_one K hK]
norm_num
let : IsProbabilityMeasure ν := ⟨hν⟩
let f : ℝ → ℝ := fun t => (|t| / pi) ^ 2
have hf : Continuous f := by dsimp [f]; fun_prop
have hp : 0 < γ / 2 := by linarith
have hpow : Continuous (fun t => f t ^ (γ / 2)) :=
hf.rpow_const (fun t => inr hp.le)
have hfi : Integrable f ν := by
apply (integrable_withDensity_iff_integrable_smul' hw hwtop).2
simpa only [w, ENNReal.toReal_ofReal (hnonneg _), smul_eq_mul, μ,
IntegrableOn] using
(show Continuous (fun t => jackson K t * f t) by fun_prop).continuousOn
|>.integrableOn_compact isCompact_Icc
have hgi : Integrable ((fun x : ℝ => x ^ (γ / 2)) ∘ f) ν := by
apply (integrable_withDensity_iff_integrable_smul' hw hwtop).2
simpa only [w, ENNReal.toReal_ofReal (hnonneg _), smul_eq_mul,
Function.comp_def, μ, IntegrableOn] using
(show Continuous (fun t => jackson K t * f t ^ (γ / 2)) by fun_prop).continuousOn
|>.integrableOn_compact isCompact_Icc
have hj := (Real.concaveOn_rpow hp.le (by linarith : γ / 2 ≤ 1)).le_map_integral
(Real.continuous_rpow_const hp.le).continuousOn isClosed_Ici
(Filter.Eventually.of_forall (fun t => sq_nonneg (|t| / pi))) hfi hgi
have hmoment : (∫ t, f t ∂ν) ≤ (2 / (K : ℝ)) ^ 2 := by
rw [hbridge]
have heq : (fun t => f t * jackson K t) =
(fun t => (t ^ 2 * jackson K t) / pi ^ 2) := by
funext t
dsimp [f]
rw [div_pow, sq_abs]
ring
rw [heq, integral_div]
apply (div_le_iff₀ (sq_pos_of_pos Real.pi_pos)).2
convert jackson_second_moment_scaled hK using 1 <;> first | rfl | ring
have hpower (x : ℝ) (hx : 0 ≤ x) : (x ^ 2) ^ (γ / 2) = x ^ γ := by
rw [← Real.rpow_natCast, ← Real.rpow_mul hx]
congr 1
ring
calc
_ = ∫ t, f t ^ (γ / 2) ∂ν := by
rw [hbridge]
apply integral_congr_ae
exact Filter.Eventually.of_forall (fun t => by
dsimp [f]
rw [hpower _ (div_nonneg (abs_nonneg t) Real.pi_pos.le)])
_ ≤ (∫ t, f t ∂ν) ^ (γ / 2) := hj
_ ≤ ((2 / (K : ℝ)) ^ 2) ^ (γ / 2) :=
Real.rpow_le_rpow (integral_nonneg (fun t => sq_nonneg _)) hmoment hp.le
_ = _ := hpower _ (by positivity)
5 supporting declarations (lemmas, instances)
-
weighted_jraw_le_chebyshevtheorem — On the principal period, at a positive kernel order, the raw squared-angle weighted kernel is bounded by π² times the squared Chebyshev sine quotient.hypothesesProof (Lean source)
theorem weighted_jraw_le_chebyshev {K : ℕ} (hK : 0 < K) {t : ℝ} (ht : t ∈ Icc (-pi) pi) : t ^ 2 * jraw K t ≤ pi ^ 2 * (U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 2 := by have hhalf : |t / 2| ≤ pi / 2 := by rw [abs_div] norm_num exact div_le_div_of_nonneg_right (abs_le.mpr ht) (by norm_num) have hchord := Real.mul_abs_le_abs_sin hhalf have habs : |t| ≤ pi * |sin (t / 2)| := by have hpi := Real.pi_pos rw [abs_div] at hchord norm_num at hchord field_simp at hchord nlinarith have ht2 : t ^ 2 ≤ pi ^ 2 * sin (t / 2) ^ 2 := by have hs := mul_self_le_mul_self (abs_nonneg t) habs simpa [← pow_two, mul_pow, sq_abs] using hs let u := (U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) have hu : u * sin (t / 2) = sin ((K : ℝ) * t / 2) := by have hc : (((K - 1 : ℕ) : ℤ) : ℝ) + 1 = (K : ℝ) := by exact_mod_cast (show K - 1 + 1 = K by omega) have hu := Polynomial.Chebyshev.U_real_cos (t / 2) ((K - 1 : ℕ) : ℤ) rw [hc] at hu simpa [u, mul_div_assoc] using hu have hs2 : sin ((K : ℝ) * t / 2) ^ 2 ≤ 1 := by nlinarith [Real.neg_one_le_sin ((K : ℝ) * t / 2), Real.sin_le_one ((K : ℝ) * t / 2)] have hbase : t ^ 2 * u ^ 2 ≤ pi ^ 2 := by calc _ ≤ (pi ^ 2 * sin (t / 2) ^ 2) * u ^ 2 := mul_le_mul_of_nonneg_right ht2 (sq_nonneg u) _ = pi ^ 2 * sin ((K : ℝ) * t / 2) ^ 2 := by rw [← hu]; ring _ ≤ pi ^ 2 := by nlinarith [sq_nonneg pi] rw [jraw_eq_chebyshev K hK t] change t ^ 2 * u ^ 4 ≤ pi ^ 2 * u ^ 2 calc _ = (t ^ 2 * u ^ 2) * u ^ 2 := by ring _ ≤ _ := mul_le_mul_of_nonneg_right hbase (sq_nonneg u) -
integral_chebyshev_sqtheorem — At a positive order, the squared Chebyshev sine quotient has period integral 2π times that order.hypothesesK :ℕhK :0 < KProof (Lean source)
theorem integral_chebyshev_sq {K : ℕ} (hK : 0 < K) : (∫ t in Icc (-pi) pi, (U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 2) = 2 * pi * (K : ℝ) := by have hfun : (fun t : ℝ => (U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 2) = fun t => (K : ℝ) + 2 * ∑ j ∈ range (K - 1), ((K - 1 : ℕ) - j : ℝ) * cos (((j + 1 : ℕ) : ℝ) * t) := by funext t rw [cheb_U_sq_eval (K - 1) t] congr 2 norm_cast omega rw [hfun] have hiConst : IntegrableOn (fun _t : ℝ => (K : ℝ)) (Icc (-pi) pi) := continuous_const.continuousOn.integrableOn_compact isCompact_Icc have hiSum : IntegrableOn (fun t : ℝ => 2 * ∑ j ∈ range (K - 1), ((K - 1 : ℕ) - j : ℝ) * cos (((j + 1 : ℕ) : ℝ) * t)) (Icc (-pi) pi) := by exact (show Continuous (fun t : ℝ => 2 * ∑ j ∈ range (K - 1), ((K - 1 : ℕ) - j : ℝ) * cos (((j + 1 : ℕ) : ℝ) * t)) by fun_prop).continuousOn.integrableOn_compact isCompact_Icc rw [MeasureTheory.integral_add hiConst hiSum, MeasureTheory.integral_const_mul] have hsum : (∫ t in Icc (-pi) pi, ∑ j ∈ range (K - 1), ((K - 1 : ℕ) - j : ℝ) * cos (((j + 1 : ℕ) : ℝ) * t)) = 0 := by calc _ = ∑ j ∈ range (K - 1), ∫ t in Icc (-pi) pi, ((K - 1 : ℕ) - j : ℝ) * cos (((j + 1 : ℕ) : ℝ) * t) := MeasureTheory.integral_finsetSum (range (K - 1)) (by intro j hj exact (show Continuous (fun t : ℝ => ((K - 1 : ℕ) - j : ℝ) * cos (((j + 1 : ℕ) : ℝ) * t)) by fun_prop).continuousOn |>.integrableOn_compact isCompact_Icc) _ = 0 := by apply Finset.sum_eq_zero intro j hj rw [MeasureTheory.integral_const_mul, integral_cos_nat (j + 1) (by omega)] ring rw [hsum] rw [integral_const_Icc] ring -
jackson_second_moment_scaledtheorem — At a positive kernel order, the Jackson squared-angle moment is at most the square of 2π divided by the order.hypothesesK :ℕhK :0 < KProof (Lean source)
theorem jackson_second_moment_scaled {K : ℕ} (hK : 0 < K) : (∫ t in Icc (-pi) pi, t ^ 2 * jackson K t) ≤ (2 * pi / (K : ℝ)) ^ 2 := by have hiLeft : IntegrableOn (fun t => t ^ 2 * jraw K t) (Icc (-pi) pi) := (show Continuous (fun t => t ^ 2 * jraw K t) by fun_prop).continuousOn |>.integrableOn_compact isCompact_Icc have hiRight : IntegrableOn (fun t => pi ^ 2 * (U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 2) (Icc (-pi) pi) := (show Continuous (fun t => pi ^ 2 * (U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 2) by fun_prop).continuousOn |>.integrableOn_compact isCompact_Icc have hraw : (∫ t in Icc (-pi) pi, t ^ 2 * jraw K t) ≤ 2 * pi ^ 3 * (K : ℝ) := by calc _ ≤ ∫ t in Icc (-pi) pi, pi ^ 2 * (U ℝ ((K - 1 : ℕ) : ℤ)).eval (cos (t / 2)) ^ 2 := setIntegral_mono_on hiLeft hiRight measurableSet_Icc (fun t ht => weighted_jraw_le_chebyshev hK ht) _ = _ := by rw [integral_const_mul, integral_chebyshev_sq hK] ring have hmass := jrawMass_lower K hK have hmasspos := jrawMass_pos K hK have hKR : (0 : ℝ) < K := by exact_mod_cast hK rw [show (fun t => t ^ 2 * jackson K t) = (fun t => (t ^ 2 * jraw K t) / jrawMass K) by funext t; simp only [jackson]; ring, integral_div] apply (div_le_iff₀ hmasspos).2 calc _ ≤ 2 * pi ^ 3 * (K : ℝ) := hraw _ ≤ (2 * pi / (K : ℝ)) ^ 2 * ((4 * pi / 3) * (K : ℝ) ^ 3) := by field_simp nlinarith [Real.pi_pos] _ ≤ (2 * pi / (K : ℝ)) ^ 2 * jrawMass K := mul_le_mul_of_nonneg_left hmass (sq_nonneg _) -
matchedOrder_boundstheorem — For a positive rank, its matched Jackson order is positive and has degree strictly below rank.hypothesesk :ℕhk :1 ≤ kconclusionconclusion 10 < (k + 1) / 2conclusion 22 * ((k + 1) / 2 - 1) < kProof (Lean source)
theorem matchedOrder_bounds {k : ℕ} (hk : 1 ≤ k) : 0 < (k + 1) / 2 ∧ 2 * ((k + 1) / 2 - 1) < k := by omega -
matchedOrder_constant_fivetheorem — For a positive rank and an exponent between zero and one, the matched-order moment bound is at most five times rank to minus that exponent.hypothesesk :ℕγ :ℝhk :1 ≤ khγ :0 < γhγ1 :γ ≤ 1conclusion(2 / (((k + 1) / 2 : ℕ) : ℝ)) ^ γ ≤ 5 * (k : ℝ) ^ (-γ)Proof (Lean source)
theorem matchedOrder_constant_five {k : ℕ} {γ : ℝ} (hk : 1 ≤ k) (hγ : 0 < γ) (hγ1 : γ ≤ 1) : (2 / (((k + 1) / 2 : ℕ) : ℝ)) ^ γ ≤ 5 * (k : ℝ) ^ (-γ) := by have hkR : (0 : ℝ) < k := by exact_mod_cast (by omega : 0 < k) have hKR : (0 : ℝ) < ((k + 1) / 2 : ℕ) := by exact_mod_cast (matchedOrder_bounds hk).1 have hrank : (k : ℝ) ≤ 2 * (((k + 1) / 2 : ℕ) : ℝ) := by exact_mod_cast (by omega : k ≤ 2 * ((k + 1) / 2)) have hratio : 2 / (((k + 1) / 2 : ℕ) : ℝ) ≤ 4 / (k : ℝ) := by apply (div_le_div_iff₀ hKR hkR).2 linarith have hfour : (4 : ℝ) ^ γ ≤ 4 := by simpa only [Real.rpow_one] using Real.rpow_le_rpow_of_exponent_le (by norm_num : (1 : ℝ) ≤ 4) hγ1 calc _ ≤ (4 / (k : ℝ)) ^ γ := Real.rpow_le_rpow (by positivity) hratio hγ.le _ = (4 : ℝ) ^ γ * (k : ℝ) ^ (-γ) := by rw [Real.div_rpow (by norm_num) hkR.le, Real.rpow_neg hkR.le, div_eq_mul_inv] _ ≤ 5 * (k : ℝ) ^ (-γ) := mul_le_mul_of_nonneg_right (hfour.trans (by norm_num)) (Real.rpow_nonneg hkR.le _)
Norms 1 core · 6 supporting These analytic bridges keep continuous-on-interval assumptions local, and identify the extended square-integral norm with the real square-root norm. ★ l2Norm_le_of_abs_le
Uniform measure and L² bridges
These analytic bridges keep continuous-on-interval assumptions local, and identify the extended square-integral norm with the real square-root norm. No spectral or Jackson arguments are used in this module.
theorem l2Norm_le_of_abs_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
A function continuous on the interval whose absolute value is bounded there by a nonnegative constant has L² norm at most that constant.
Formal statement
hypotheses
conclusion
l2Norm g ≤ B
Proof (Lean source)
theorem l2Norm_le_of_abs_le {g : ℝ → ℝ} {B : ℝ}
(hg : ContinuousOn g (Icc (0 : ℝ) 1)) (hB0 : 0 ≤ B)
(hB : ∀ x ∈ Icc (0 : ℝ) 1, |g x| ≤ B) : l2Norm g ≤ B := by
unfold l2Norm
apply (Real.sqrt_le_iff).2
refine ⟨hB0, ?_⟩
have hi := integral_mono_ae (integrable_sq_of_continuousOn hg)
(integrable_const (B ^ 2) : Integrable (fun _ : ℝ => B ^ 2) uniformMeasure)
((ae_restrict_iff' measurableSet_Icc).2 (ae_of_all _ fun x hx =>
pow_le_pow_left₀ (abs_nonneg (g x)) (hB x hx) 2))
simpa [uniformMeasure, Real.volume_Icc] using hi
6 supporting declarations (lemmas, instances)
-
uniformMeasure_univtheorem — Uniform design on the unit interval has total mass one.conclusionuniformMeasure univ = 1Proof (Lean source)
-
uniformMeasure_isProbabilityMeasureinstance — Uniform design is a probability measure.instancegiven by⟨uniformMeasure_univ⟩ -
uniformIntegral_eq_intervalIntegraltheorem — The uniform integral of a real function equals its interval integral from zero to one, without additional regularity assumptions.hypothesesg :ℝ → ℝconclusion(∫ x, g x ∂uniformMeasure) = ∫ x in (0 : ℝ)..1, g xProof (Lean source)
theorem uniformIntegral_eq_intervalIntegral (g : ℝ → ℝ) : (∫ x, g x ∂uniformMeasure) = ∫ x in (0 : ℝ)..1, g x := by rw [uniformMeasure, integral_Icc_eq_integral_Ioc, intervalIntegral.integral_of_le (by norm_num : (0 : ℝ) ≤ 1)] -
extendedL2Norm_eq_eLpNormtheorem — The extended square-integral norm of a real function equals Mathlib's L² seminorm under uniform design.Proof (Lean source)
theorem extendedL2Norm_eq_eLpNorm (g : ℝ → ℝ) : extendedL2Norm g = eLpNorm g 2 uniformMeasure := by rw [eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num) (by simp)] simp only [ENNReal.toReal_ofNat] unfold extendedL2Norm congr 1 apply lintegral_congr intro x rw [ENNReal.ofReal_pow (abs_nonneg (g x)) 2] simp [Real.enorm_eq_ofReal_abs] -
integrable_sq_of_continuousOntheorem — A function continuous on the closed unit interval has integrable squared absolute value under uniform design.hypothesesg :ℝ → ℝhg :ContinuousOn g (Icc (0 : ℝ) 1)conclusionIntegrable (fun x => |g x| ^ 2) uniformMeasureProof (Lean source)
theorem integrable_sq_of_continuousOn {g : ℝ → ℝ} (hg : ContinuousOn g (Icc (0 : ℝ) 1)) : Integrable (fun x => |g x| ^ 2) uniformMeasure := by exact (hg.abs.pow 2).integrableOn_Icc -
extendedL2Norm_eq_ofRealtheorem — For a function continuous on the closed unit interval, the extended L² norm is the nonnegative embedding of its real L² norm.Proof (Lean source)
theorem extendedL2Norm_eq_ofReal {g : ℝ → ℝ} (hg : ContinuousOn g (Icc (0 : ℝ) 1)) : extendedL2Norm g = ofReal (l2Norm g) := by unfold extendedL2Norm l2Norm rw [← ofReal_integral_eq_lintegral_ofReal (integrable_sq_of_continuousOn hg) (ae_of_all _ fun x => sq_nonneg |g x|)] rw [ENNReal.ofReal_rpow_of_nonneg (integral_nonneg fun x => sq_nonneg |g x|) (by norm_num), Real.sqrt_eq_rpow]
Orthogonality 1 core · 5 supporting The orthogonal projection is the actual finite integral formula from Definitions. ★ cosineProjection_bestApproximation
Cosine orthogonality and explicit best approximation
The orthogonal projection is the actual finite integral formula from Definitions. The Pythagorean identity supplies best approximation against every rank-k cosine polynomial, without assuming that a separately chosen Hilbert projection agrees with the formula. No completeness of the infinite cosine system is needed.
theorem cosineProjection_bestApproximation reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
The projection of a continuous target has L² error no greater than any competitor that belongs to the same cosine span.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem cosineProjection_bestApproximation {f p : ℝ → ℝ} {k : ℕ}
(hf : ContinuousOn f (Icc (0 : ℝ) 1))
(hspan : InCosineSpan k p) :
l2Norm (fun x => f x - cosineProjection k f x) ≤ l2Norm (fun x => f x - p x) := by
obtain ⟨a, ha⟩ := hspan
have heq : (∫ x, |f x - p x| ^ 2 ∂uniformMeasure) =
∫ x, |f x - cosinePolynomial k a x| ^ 2 ∂uniformMeasure := by
apply integral_congr_ae
apply (ae_restrict_iff' measurableSet_Icc).2
exact ae_of_all _ (fun x hx => by dsimp only; rw [ha x hx])
unfold l2Norm
apply Real.sqrt_le_sqrt
rw [heq, cosineProjection_pythagoras k a hf]
exact le_add_of_nonneg_right (integral_nonneg fun x => sq_nonneg _)
5 supporting declarations (lemmas, instances)
-
continuous_cosineBasistheorem — Each normalized cosine mode is continuous on the real line.Proof (Lean source)
@[fun_prop] theorem continuous_cosineBasis (j : ℕ) : Continuous (cosineBasis j) := by unfold cosineBasis split_ifs <;> fun_prop -
continuous_cosinePolynomialtheorem — Every finite cosine polynomial is continuous on the real line.Proof (Lean source)
@[fun_prop] theorem continuous_cosinePolynomial (k : ℕ) (a : ℕ → ℝ) : Continuous (cosinePolynomial k a) := by unfold cosinePolynomial fun_prop -
cosineBasis_orthonormaltheorem — The uniform integral of two normalized cosine modes is one for equal indices and zero for distinct indices.hypothesesi j :ℕconclusion(∫ x, cosineBasis i x * cosineBasis j x ∂uniformMeasure) = if i = j then 1 else 0Proof (Lean source)
theorem cosineBasis_orthonormal (i j : ℕ) : (∫ x, cosineBasis i x * cosineBasis j x ∂uniformMeasure) = if i = j then 1 else 0 := by have hcos (m : ℤ) : (∫ x, cos (pi * (m : ℝ) * x) ∂uniformMeasure) = if m = 0 then 1 else 0 := by rw [uniformIntegral_eq_intervalIntegral] by_cases hm : m = 0 · simp [hm] · have hm0 : pi * (m : ℝ) ≠ 0 := mul_ne_zero Real.pi_ne_zero (by exact_mod_cast hm) rw [if_neg hm, intervalIntegral.integral_comp_mul_left _ hm0, integral_cos] simp only [mul_one, mul_zero, Real.sin_zero, sub_zero] rw [mul_comm pi, Real.sin_int_mul_pi] simp have hraw : (∫ x, cos (pi * (i : ℝ) * x) * cos (pi * (j : ℝ) * x) ∂uniformMeasure) = ((if i = j then 1 else 0) + (if i = 0 ∧ j = 0 then 1 else 0)) / 2 := by have hpoint (x : ℝ) : cos (pi * (i : ℝ) * x) * cos (pi * (j : ℝ) * x) = (cos (pi * ((i : ℤ) - j : ℤ) * x) + cos (pi * ((i : ℤ) + j : ℤ) * x)) / 2 := by push_cast rw [show pi * ((i : ℝ) - j) * x = pi * i * x - pi * j * x by ring, show pi * ((i : ℝ) + j) * x = pi * i * x + pi * j * x by ring, Real.cos_sub, Real.cos_add] ring simp_rw [hpoint] rw [integral_div] have h₁ : Integrable (fun x : ℝ => cos (pi * ((i : ℤ) - j : ℤ) * x)) uniformMeasure := (show Continuous (fun x : ℝ => cos (pi * ((i : ℤ) - j : ℤ) * x)) by fun_prop).continuousOn.integrableOn_Icc have h₂ : Integrable (fun x : ℝ => cos (pi * ((i : ℤ) + j : ℤ) * x)) uniformMeasure := (show Continuous (fun x : ℝ => cos (pi * ((i : ℤ) + j : ℤ) * x)) by fun_prop).continuousOn.integrableOn_Icc rw [integral_add h₁ h₂, hcos, hcos] have hsub : (i : ℤ) - j = 0 ↔ i = j := by omega have hadd : (i : ℤ) + j = 0 ↔ i = 0 ∧ j = 0 := by omega simp only [hsub, hadd] by_cases hi : i = 0 <;> by_cases hj : j = 0 · simp [cosineBasis, hi, hj] · subst i simp only [cosineBasis, if_true, if_neg hj, one_mul] rw [integral_const_mul] simpa [hj, eq_comm] using congrArg (sqrt 2 * ·) (hcos (j : ℤ)) · subst j simp only [cosineBasis, if_true, if_neg hi, mul_one] rw [integral_const_mul] simpa [hi] using congrArg (sqrt 2 * ·) (hcos (i : ℤ)) · simp only [cosineBasis, if_neg hi, if_neg hj] have hs : sqrt 2 * sqrt 2 = 2 := Real.mul_self_sqrt (by norm_num) simp_rw [show ∀ x : ℝ, (sqrt 2 * cos (pi * i * x)) * (sqrt 2 * cos (pi * j * x)) = 2 * (cos (pi * i * x) * cos (pi * j * x)) by intro x calc _ = (sqrt 2 * sqrt 2) * (cos (pi * i * x) * cos (pi * j * x)) := by ring _ = _ := by rw [hs]] rw [integral_const_mul, hraw] simp [hi] split_ifs <;> norm_num -
cosineProjection_residual_orthogonaltheorem — The residual of a continuous target after rank-k projection has zero coefficient in every retained mode, for an index below rank.hypothesesconclusion(∫ x, (f x - cosineProjection k f x) * cosineBasis j x ∂uniformMeasure) = 0Proof (Lean source)
theorem cosineProjection_residual_orthogonal {f : ℝ → ℝ} {k j : ℕ} (hf : ContinuousOn f (Icc (0 : ℝ) 1)) (hj : j < k) : (∫ x, (f x - cosineProjection k f x) * cosineBasis j x ∂uniformMeasure) = 0 := by have hfb : Integrable (fun x => f x * cosineBasis j x) uniformMeasure := (hf.mul (continuous_cosineBasis j).continuousOn).integrableOn_Icc have hpb : Integrable (fun x => cosineProjection k f x * cosineBasis j x) uniformMeasure := ((continuous_cosinePolynomial k (cosineCoefficient f)).continuousOn.mul (continuous_cosineBasis j).continuousOn).integrableOn_Icc simp_rw [sub_mul] rw [integral_sub hfb hpb] have hproj : (∫ x, cosineProjection k f x * cosineBasis j x ∂uniformMeasure) = cosineCoefficient f j := by unfold cosineProjection cosinePolynomial simp_rw [Finset.sum_mul, mul_assoc] rw [integral_finsetSum _ (fun i hi => (show Integrable (fun x => cosineCoefficient f i * (cosineBasis i x * cosineBasis j x)) uniformMeasure from (((continuous_cosineBasis i).mul (continuous_cosineBasis j)).continuousOn.integrableOn_Icc).const_mul _))] simp_rw [integral_const_mul, cosineBasis_orthonormal] simp [Finset.mem_range.mpr hj] rw [hproj] simp [cosineCoefficient] -
cosineProjection_pythagorastheorem — For a continuous target and arbitrary cosine coefficients, the squared error decomposes into projection error plus squared distance from the projection to that polynomial.hypothesesconclusion(∫ x, |f x - cosinePolynomial k a x| ^ 2 ∂uniformMeasure)= (∫ x, |f x - cosineProjection k f x| ^ 2 ∂uniformMeasure)+ (∫ x, |cosineProjection k f x - cosinePolynomial k a x| ^ 2 ∂uniformMeasure)Proof (Lean source)
theorem cosineProjection_pythagoras {f : ℝ → ℝ} (k : ℕ) (a : ℕ → ℝ) (hf : ContinuousOn f (Icc (0 : ℝ) 1)) : (∫ x, |f x - cosinePolynomial k a x| ^ 2 ∂uniformMeasure) = (∫ x, |f x - cosineProjection k f x| ^ 2 ∂uniformMeasure) + (∫ x, |cosineProjection k f x - cosinePolynomial k a x| ^ 2 ∂uniformMeasure) := by let r := fun x => f x - cosineProjection k f x let d := fun x => cosineProjection k f x - cosinePolynomial k a x have hr : ContinuousOn r (Icc (0 : ℝ) 1) := hf.sub (continuous_cosinePolynomial k (cosineCoefficient f)).continuousOn have hd : ContinuousOn d (Icc (0 : ℝ) 1) := (continuous_cosinePolynomial k (cosineCoefficient f)).continuousOn.sub (continuous_cosinePolynomial k a).continuousOn have hcross : (∫ x, r x * d x ∂uniformMeasure) = 0 := by have hpoint (x : ℝ) : r x * d x = ∑ j ∈ range k, (cosineCoefficient f j - a j) * (r x * cosineBasis j x) := by dsimp [d, cosineProjection, cosinePolynomial] rw [← Finset.sum_sub_distrib, Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring simp_rw [hpoint] rw [integral_finsetSum _ (fun j hj => (show Integrable (fun x => (cosineCoefficient f j - a j) * (r x * cosineBasis j x)) uniformMeasure from (hr.mul (continuous_cosineBasis j).continuousOn).integrableOn_Icc.const_mul _))] apply Finset.sum_eq_zero intro j hj rw [integral_const_mul, cosineProjection_residual_orthogonal hf (Finset.mem_range.mp hj), mul_zero] have hpoint (x : ℝ) : |f x - cosinePolynomial k a x| ^ 2 = |r x| ^ 2 + |d x| ^ 2 + 2 * (r x * d x) := by dsimp [r, d] simp only [sq_abs] ring simp_rw [hpoint] have hrd : Integrable (fun x => 2 * (r x * d x)) uniformMeasure := (hr.mul hd).integrableOn_Icc.const_mul 2 have hsum : Integrable (fun x => |r x| ^ 2 + |d x| ^ 2) uniformMeasure := (integrable_sq_of_continuousOn hr).add (integrable_sq_of_continuousOn hd) rw [integral_add hsum hrd, integral_add (integrable_sq_of_continuousOn hr) (integrable_sq_of_continuousOn hd), integral_const_mul, hcross] simp [r, d]
Seminorm 1 core · 3 supporting The supremum definition is related to ordinary nonnegative increment bounds. ★ extended_bound_of_seminorm_top
Finite and infinite Hölder seminorm bridges
The supremum definition is related to ordinary nonnegative increment bounds. The headline theorem will split at infinity, never convert an infinite seminorm to a real number and silently replace it by zero.
theorem extended_bound_of_seminorm_top reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
With positive rank, an infinite Hölder seminorm makes the extended L² norm of any function at most five times that seminorm times k⁻γ, because the right-hand side is then infinite.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem extended_bound_of_seminorm_top {f g : ℝ → ℝ} {γ : ℝ} {k : ℕ}
(hk : 1 ≤ k) (hseminorm : holderSeminorm f γ = ⊤) :
extendedL2Norm g ≤ 5 * holderSeminorm f γ * ofReal ((k : ℝ) ^ (-γ)) := by
rw [hseminorm, ENNReal.mul_top (by norm_num),
ENNReal.top_mul (ne_of_gt (ENNReal.ofReal_pos.mpr (rank_rpow_pos hk γ)))]
exact le_top
3 supporting declarations (lemmas, instances)
-
hasHolderBound_seminormtheorem — A positive exponent and finite extended seminorm give the Hölder increment bound with its real value.hypothesesconclusionProof (Lean source)
theorem hasHolderBound_seminorm {f : ℝ → ℝ} {γ : ℝ} (hγ : 0 < γ) (hfinite : holderSeminorm f γ ≠ ⊤) : HasHolderBound f γ (holderSeminorm f γ).toReal := by intro x hx z hz by_cases heq : x = z · subst z simp [Real.zero_rpow hγ.ne'] · have hdist : 0 < |x - z| ^ γ := Real.rpow_pos_of_pos (abs_pos.mpr (sub_ne_zero.mpr heq)) _ have hne : (⟨x, hx⟩ : Icc (0 : ℝ) 1) ≠ ⟨z, hz⟩ := fun h => heq (congrArg val h) have hle : ofReal (|f x - f z| / |x - z| ^ γ) ≤ holderSeminorm f γ := le_iSup_of_le ⟨x, hx⟩ (le_iSup_of_le ⟨z, hz⟩ (le_iSup_of_le hne le_rfl)) exact (div_le_iff₀ hdist).mp ((ENNReal.ofReal_le_iff_le_toReal hfinite).mp hle) -
holderSeminorm_le_of_boundtheorem — A constant satisfying the Hölder increment inequality bounds the extended seminorm by that constant.Proof (Lean source)
theorem holderSeminorm_le_of_bound {f : ℝ → ℝ} {γ H : ℝ} (hf : HasHolderBound f γ H) : holderSeminorm f γ ≤ ofReal H := by unfold holderSeminorm refine iSup_le fun x => iSup_le fun z => iSup_le fun hne => ?_ have hdist : 0 < |(x : ℝ) - z| ^ γ := Real.rpow_pos_of_pos (abs_pos.mpr (sub_ne_zero.mpr (fun h => hne (Subtype.ext h)))) _ exact ENNReal.ofReal_le_ofReal ((div_le_iff₀ hdist).mpr (hf x x.property z z.property)) -
rank_rpow_postheorem — At a positive rank, the real power of that rank is positive, for every real exponent.hypothesesk :ℕhk :1 ≤ kγ :ℝconclusion0 < (k : ℝ) ^ (-γ)Proof (Lean source)
theorem rank_rpow_pos {k : ℕ} (hk : 1 ≤ k) (γ : ℝ) : 0 < (k : ℝ) ^ (-γ) := by exact Real.rpow_pos_of_pos (by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hk)) _
Span 1 core · 1 supporting Zero padding of coefficient sequences embeds every finite normalized cosine span in each larger rank. ★ inCosineSpan_mono
Enlarging finite cosine spans
Zero padding of coefficient sequences embeds every finite normalized cosine span in each larger rank. The rank still counts the constant mode, with no positivity assumption needed for this algebraic inclusion.
theorem inCosineSpan_mono reviewed
⚑ flagged
Causalean.Mathlib.Analysis.Approximation.Chebyshev.CosineProjection
A function in a smaller cosine span belongs to every larger cosine span, whenever the ranks are ordered.
Formal statement
Proof (Lean source)
theorem inCosineSpan_mono {m n : ℕ} {p : ℝ → ℝ}
(hmn : m ≤ n) (hp : InCosineSpan m p) : InCosineSpan n p := by
rcases hp with ⟨a, ha⟩
refine ⟨fun j => if j < m then a j else 0, ?_⟩
intro x hx
rw [cosinePolynomial_zero_pad hmn, ha x hx]
1 supporting declaration (lemmas, instances)
-
cosinePolynomial_zero_padtheorem — A cosine polynomial of smaller rank equals its zero-padded polynomial at the larger rank, at every position.hypothesesm n :ℕhmn :m ≤ na :ℕ → ℝx :ℝconclusioncosinePolynomial n (fun j => if j < m then a j else 0) x = cosinePolynomial m a xProof (Lean source)
theorem cosinePolynomial_zero_pad {m n : ℕ} (hmn : m ≤ n) (a : ℕ → ℝ) (x : ℝ) : cosinePolynomial n (fun j => if j < m then a j else 0) x = cosinePolynomial m a x := by classical unfold cosinePolynomial calc _ = ∑ j ∈ range m, (if j < m then a j else 0) * cosineBasis j x := by symm apply Finset.sum_subset (Finset.range_mono hmn) intro j hjn hjm simp only [Finset.mem_range] at hjm simp [hjm] _ = _ := by apply Finset.sum_congr rfl intro j hj simp [Finset.mem_range.mp hj]