Euclidean cutoff-covariance derivative majorant

This file constructs the cutoff-dependent positive majorant for repeated coordinate derivatives of η. It is deliberately Euclidean: periodization and integration by parts belong to later modules.

def Anderson4D.SmoothCutoff.etaCoordDirection (i : Fin dim) : R4

The unit vector in Euclidean coordinate i.

Equations

• Anderson4D.SmoothCutoff.etaCoordDirection i = Pi.single i 1

def Anderson4D.SmoothCutoff.repeatedEtaCoordDirections (r : ℕ) (i : Fin dim) : Fin r → R4

The same coordinate direction in every derivative slot.

Equations

• Anderson4D.SmoothCutoff.repeatedEtaCoordDirections r i x✝ = Anderson4D.SmoothCutoff.etaCoordDirection i

noncomputable def Anderson4D.SmoothCutoff.etaCoordDerivative (ρ : SmoothCutoff) (r : ℕ) (i : Fin dim) (x : R4) : ℝ

The r-fold derivative of η in coordinate i, evaluated through mathlib's actual iterated Fréchet derivative.

Equations

• ρ.etaCoordDerivative r i x = (iteratedFDeriv ℝ r ρ.eta x) (Anderson4D.SmoothCutoff.repeatedEtaCoordDirections r i)

theorem Anderson4D.SmoothCutoff.continuous_etaCoordDerivative (ρ : SmoothCutoff) (r : ℕ) (i : Fin dim) : Continuous (ρ.etaCoordDerivative r i)

Repeated coordinate derivatives of η are continuous.

theorem Anderson4D.SmoothCutoff.support_iteratedFDeriv_eta_subset_tsupport (ρ : SmoothCutoff) (r : ℕ) : (Function.support fun (x : R4) => iteratedFDeriv ℝ r ρ.eta x) ⊆ tsupport ρ.eta

The support of the full iterated Fréchet derivative is contained in the original covariance's topological support.

theorem Anderson4D.SmoothCutoff.iteratedFDeriv_eta_eq_zero_of_not_mem_tsupport (ρ : SmoothCutoff) (r : ℕ) {x : R4} (hx : x ∉ tsupport ρ.eta) : iteratedFDeriv ℝ r ρ.eta x = 0

Consequently the full iterated derivative vanishes outside tsupport η.

theorem Anderson4D.SmoothCutoff.etaCoordDerivative_eq_zero_of_not_mem_tsupport (ρ : SmoothCutoff) (r : ℕ) (i : Fin dim) {x : R4} (hx : x ∉ tsupport ρ.eta) : ρ.etaCoordDerivative r i x = 0

The repeated coordinate derivative also vanishes outside tsupport η.

theorem Anderson4D.SmoothCutoff.support_etaCoordDerivative_subset_tsupport (ρ : SmoothCutoff) (r : ℕ) (i : Fin dim) : Function.support (ρ.etaCoordDerivative r i) ⊆ tsupport ρ.eta

Explicit support inclusion for the scalar coordinate derivative.

theorem Anderson4D.SmoothCutoff.abs_etaCoordDerivative_le_norm_iteratedFDeriv (ρ : SmoothCutoff) (r : ℕ) (i : Fin dim) (x : R4) : |ρ.etaCoordDerivative r i x| ≤ ‖iteratedFDeriv ℝ r ρ.eta x‖

Evaluation on repeated unit coordinate vectors is bounded by the operator norm of the full iterated derivative.

theorem Anderson4D.SmoothCutoff.exists_pos_etaIteratedFDeriv_bound (ρ : SmoothCutoff) (r : ℕ) : ∃ (B : ℝ), 0 < B ∧ ∀ (x : R4), ‖iteratedFDeriv ℝ r ρ.eta x‖ ≤ B

Every fixed derivative order has a positive global operator-norm bound depending only on the named cutoff.

theorem Anderson4D.SmoothCutoff.exists_pos_auxiliaryEta_lowerBound_on_tsupport (ρ : SmoothCutoff) : ∃ (c : ℝ), 0 < c ∧ ∀ x ∈ tsupport ρ.eta, c ≤ ρ.auxiliaryCutoff.eta x

The auxiliary covariance has a strictly positive lower bound on the compact support of the original covariance.

Uniform constants through order eight

theorem Anderson4D.SmoothCutoff.exists_pos_etaIteratedFDeriv_bound_upto_eight (ρ : SmoothCutoff) : ∃ (B : ℝ), 0 < B ∧ ∀ r ≤ 8, ∀ (x : R4), ‖iteratedFDeriv ℝ r ρ.eta x‖ ≤ B

A single positive operator-norm bound for derivative orders 0,...,8. It depends on ρ, as it must.

noncomputable def Anderson4D.SmoothCutoff.etaIteratedFDerivBound (ρ : SmoothCutoff) : ℝ

The named numerator constant, selected after fixing ρ.

Equations

• ρ.etaIteratedFDerivBound = Classical.choose ⋯

theorem Anderson4D.SmoothCutoff.etaIteratedFDerivBound_pos (ρ : SmoothCutoff) : 0 < ρ.etaIteratedFDerivBound

theorem Anderson4D.SmoothCutoff.norm_iteratedFDeriv_eta_le_etaIteratedFDerivBound (ρ : SmoothCutoff) {r : ℕ} (hr : r ≤ 8) (x : R4) : ‖iteratedFDeriv ℝ r ρ.eta x‖ ≤ ρ.etaIteratedFDerivBound

noncomputable def Anderson4D.SmoothCutoff.auxiliaryEtaLowerBound (ρ : SmoothCutoff) : ℝ

The named positive lower bound for the auxiliary covariance on tsupport η.

Equations

• ρ.auxiliaryEtaLowerBound = Classical.choose ⋯

theorem Anderson4D.SmoothCutoff.auxiliaryEtaLowerBound_pos (ρ : SmoothCutoff) : 0 < ρ.auxiliaryEtaLowerBound

theorem Anderson4D.SmoothCutoff.auxiliaryEtaLowerBound_le (ρ : SmoothCutoff) {x : R4} (hx : x ∈ tsupport ρ.eta) : ρ.auxiliaryEtaLowerBound ≤ ρ.auxiliaryCutoff.eta x

noncomputable def Anderson4D.SmoothCutoff.etaDerivativeMajorantConstant (ρ : SmoothCutoff) : ℝ

The cutoff-dependent constant in the Euclidean derivative majorant.

Equations

• ρ.etaDerivativeMajorantConstant = ρ.etaIteratedFDerivBound / ρ.auxiliaryEtaLowerBound

theorem Anderson4D.SmoothCutoff.etaDerivativeMajorantConstant_pos (ρ : SmoothCutoff) : 0 < ρ.etaDerivativeMajorantConstant

theorem Anderson4D.SmoothCutoff.abs_etaCoordDerivative_le_majorant (ρ : SmoothCutoff) {r : ℕ} (hr : r ≤ 8) (i : Fin dim) (x : R4) : |ρ.etaCoordDerivative r i x| ≤ ρ.etaDerivativeMajorantConstant * ρ.auxiliaryCutoff.eta x

Every repeated coordinate derivative through order eight is dominated globally by the covariance of the named auxiliary cutoff.