Explicit estimates for the construction seminorm and time cutoffs.

theorem AVenhance.Infra.Construction.barNorm_eq_snorm (f : Homogenization.Vec 2 → ℝ) (n : ℕ) (R : ℝ) (hf : ContDiff ℝ (↑n) f) : barNorm n R f = FaaDiBruno.snorm f n R

The Appendix B seminorm uses the same coordinate derivatives as the norm.

theorem AVenhance.Infra.Construction.scaledCutoff_deriv_le {f : ℝ → ℝ} {N : ℕ} {C τ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hb : ∀ j ≤ N, ∀ (t : ℝ), |iteratedDeriv j f t| ≤ C) (hτ : 0 < τ) (k : ℤ) {j : ℕ} (hj : j ≤ N) (t : ℝ) : τ ^ j * |iteratedDeriv j (scaledCutoff f τ k) t| ≤ C

The small cutoff scaling cancels its derivative factor exactly.

theorem AVenhance.Infra.Construction.zetaMK_deriv_le {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : tau β I.Λ m ^ j * |iteratedDeriv j (I.zetaMK m k) t| ≤ I.Czeta

e.zeta.mk, with the original ingredient constant.

theorem AVenhance.Infra.Construction.ExplicitBarNorm.factorial_coefficient_le_five (n : ℕ) : (↑n + 1) ^ 2 / ↑n.factorial ≤ 5

theorem AVenhance.Infra.Construction.sine_coordinate_partial_le (A ω : ℝ) (hA : 0 ≤ A) (hω : 0 ≤ ω) (i : Fin 2) (n : ℕ) (x : Homogenization.Vec 2) (J : Fin n → Fin 2) : ‖(iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => A * Real.sin (ω * y i)) x) fun (j : Fin n) => Homogenization.basisVec (J j)‖ ≤ A * ω ^ n

A coordinate sine has no dimension loss in the derivative bound.

theorem AVenhance.Infra.Construction.barNorm_le_of_partial_le (f : Homogenization.Vec 2 → ℝ) (n : ℕ) (R B : ℝ) (hf : ContDiff ℝ (↑n) f) (hb : ∀ (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (J j)‖ ≤ B) : barNorm n R f ≤ ENNReal.ofReal ((↑n + 1) ^ 2 / ↑n.factorial) * (ENNReal.ofReal R)⁻¹ ^ n * ENNReal.ofReal B

Turning pointwise coordinate derivative bounds into the seminorm.

theorem AVenhance.Infra.Construction.barNorm_le_five_of_partial_le (f : Homogenization.Vec 2 → ℝ) (n : ℕ) {R A : ℝ} (hf : ContDiff ℝ (↑n) f) (hR : 0 < R) (hA : 0 ≤ A) (hb : ∀ (x : Homogenization.Vec 2) (J : Fin n → Fin 2), ‖(iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (J j)‖ ≤ A * R ^ n) : barNorm n R f ≤ ENNReal.ofReal (5 * A)

A geometric derivative bound yields the source constant five at every order.

theorem AVenhance.Infra.Construction.barNorm_sine_le (A ω : ℝ) (hA : 0 ≤ A) (hω : 0 ≤ ω) (i : Fin 2) (n : ℕ) {R : ℝ} (hR : 0 < R) (hωR : ω ≤ R) : (barNorm n R fun (x : Homogenization.Vec 2) => A * Real.sin (ω * x i)) ≤ ENNReal.ofReal (5 * A)

Explicit barred norm for an arbitrary coordinate sine and a larger radius.

theorem AVenhance.Infra.Construction.ExplicitBarNorm.psi_sine_form {β : ℝ} {Λ m : ℕ} (k : ℤ) (x : Homogenization.Vec 2) : psi β Λ m k x = a β Λ m * epsilon β Λ m ^ 2 * if k % 4 = 1 then Real.sin (2 * Real.pi / epsilon β Λ m * x 0) else if k % 4 = 3 then Real.sin (2 * Real.pi / epsilon β Λ m * x 1) else 0

theorem AVenhance.Infra.Construction.psi_barNorm_le_of_parameters {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (m : ℕ) (k : ℤ) (n : ℕ) {R : ℝ} (hR : 2 * Real.pi / epsilon β Λ m ≤ R) : barNorm n R (psi β Λ m k) ≤ ENNReal.ofReal (5 * a β Λ m * epsilon β Λ m ^ 2)

e.psimk.snorm, on the norm, for every derivative order and larger radii.

theorem AVenhance.Infra.Construction.psi_barNorm_le {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) (n : ℕ) {R : ℝ} (hR : 2 * Real.pi / epsilon β I.Λ m ≤ R) : barNorm n R (psi β I.Λ m k) ≤ ENNReal.ofReal (5 * a β I.Λ m * epsilon β I.Λ m ^ 2)

Ingredient-package specialization of the scalar shear estimate.

theorem AVenhance.Infra.Construction.continuous_eLpNorm_top_eq_iSup (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) : MeasureTheory.eLpNorm f ⊤ MeasureTheory.volume = ⨆ (x : Homogenization.Vec 2), ‖f x‖ₑ

Continuous derivatives allow the essential supremum to be evaluated pointwise.

theorem AVenhance.Infra.Construction.barNorm_eq_pointwise (f : Homogenization.Vec 2 → ℝ) (n : ℕ) (R : ℝ) (hf : ContDiff ℝ (↑n) f) : barNorm n R f = ENNReal.ofReal ((↑n + 1) ^ 2 / ↑n.factorial) * (ENNReal.ofReal R)⁻¹ ^ n * ⨆ (J : Fin n → Fin 2), ⨆ (x : Homogenization.Vec 2), ‖(iteratedFDeriv ℝ n f x) fun (j : Fin n) => Homogenization.basisVec (J j)‖ₑ

A pointwise presentation of the exact norm.

theorem AVenhance.Infra.Construction.barNorm_add_le (f g : Homogenization.Vec 2 → ℝ) (n : ℕ) (R : ℝ) (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) : barNorm n R (f + g) ≤ barNorm n R f + barNorm n R g

Addition on the seminorm has constant one.

theorem AVenhance.Infra.Construction.timeProduct_deriv_le {f g : ℝ → ℝ} {N : ℕ} {C D s r : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hC : 0 ≤ C) (_hD : 0 ≤ D) (hs : 0 ≤ s) (_hr : 0 ≤ r) (hbF : ∀ i ≤ N, ∀ (t : ℝ), |iteratedDeriv i f t| ≤ C * s ^ i) (hbG : ∀ i ≤ N, ∀ (t : ℝ), |iteratedDeriv i g t| ≤ D * r ^ i) {j : ℕ} (hj : j ≤ N) (t : ℝ) : |iteratedDeriv j (f * g) t| ≤ C * D * (s + r) ^ j

Leibniz with geometric derivative bounds; the rates add exactly.

theorem AVenhance.Infra.Construction.derivative_envelope {f : ℝ → ℝ} {τ C : ℝ} (hτ : 0 < τ) (j : ℕ) (hb : ∀ (t : ℝ), τ ^ j * |iteratedDeriv j f t| ≤ C) (t : ℝ) : |iteratedDeriv j f t| ≤ C * τ⁻¹ ^ j

A weighted derivative estimate is equivalently an inverse-rate envelope.

theorem AVenhance.Infra.Construction.scaled_timeProduct_deriv_le {f g : ℝ → ℝ} {N : ℕ} {C D τ σ : ℝ} (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (hC : 0 ≤ C) (hD : 0 ≤ D) (hτ : 0 < τ) (hσ : 0 < σ) (hbF : ∀ i ≤ N, ∀ (t : ℝ), τ ^ i * |iteratedDeriv i f t| ≤ C) (hbG : ∀ i ≤ N, ∀ (t : ℝ), σ ^ i * |iteratedDeriv i g t| ≤ D) {j : ℕ} (hj : j ≤ N) (t : ℝ) : |iteratedDeriv j (f * g) t| ≤ C * D * (τ⁻¹ + σ⁻¹) ^ j

The product bound in time is uniform through Nstar, with explicit constants.

theorem AVenhance.Infra.Construction.zetaMK_hatZetaML_product_deriv_le {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (k l : ℤ) {j : ℕ} (hj : j ≤ Nstar β) (t : ℝ) : |iteratedDeriv j (I.zetaMK m k * I.hatZetaML m l) t| ≤ I.Czeta * I.Chat * ((tau β I.Λ m)⁻¹ + (tauP β I.Λ m)⁻¹) ^ j

Construction cutoff product, with exact small and large transition rates.

theorem AVenhance.Infra.Construction.barNorm_sum_le {ι : Type u_1} (S : Finset ι) (f : ι → Homogenization.Vec 2 → ℝ) (n : ℕ) (R : ℝ) (hf : ∀ i ∈ S, ContDiff ℝ (↑n) (f i)) : barNorm n R (∑ i ∈ S, f i) ≤ ∑ i ∈ S, barNorm n R (f i)

Finite sums retain constant one, as needed after time-cutoff localization.