Minkowski inequalities in the exact periodic cell norms used by the two T-iterate lemmas. Vector-valued gradients use PiLp 2, so their pointwise norm is the Euclidean norm from the vecNormSq definition.

theorem AVenhance.Infra.Section4.TLemmasNorm.lp_norm_sq_eq_integral {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {μ : MeasureTheory.Measure α} {f : α → E} (hf : MeasureTheory.MemLp f 2 μ) : ‖MeasureTheory.MemLp.toLp f hf‖ ^ 2 = ∫ (x : α), ‖f x‖ ^ 2 ∂μ

theorem AVenhance.Infra.Section4.TLemmasNorm.lp_norm_eq_sqrt_integral {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [InnerProductSpace ℝ E] {μ : MeasureTheory.Measure α} {f : α → E} (hf : MeasureTheory.MemLp f 2 μ) : ‖MeasureTheory.MemLp.toLp f hf‖ = √(∫ (x : α), ‖f x‖ ^ 2 ∂μ)

theorem AVenhance.Infra.Section4.sqrt_l2NormSq_add_le {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : √(l2NormSq fun (x : Homogenization.Vec 2) => f x + g x) ≤ √(l2NormSq f) + √(l2NormSq g)

The cell scalar L² norm is subadditive.

theorem AVenhance.Infra.Section4.TLemmasNorm.memLp_finset_sum {ι : Type u_1} {α : Type u_2} {E : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {s : Finset ι} {f : ι → α → E} (hf : ∀ i ∈ s, MeasureTheory.MemLp (f i) p μ) : MeasureTheory.MemLp (fun (x : α) => ∑ i ∈ s, f i x) p μ

theorem AVenhance.Infra.Section4.sqrt_l2NormSq_finset_sum_le {ι : Type u_1} (s : Finset ι) (f : ι → Homogenization.Vec 2 → ℝ) (hf : ∀ i ∈ s, Homogenization.MemL2On unitCube (f i)) : √(l2NormSq fun (x : Homogenization.Vec 2) => ∑ i ∈ s, f i x) ≤ ∑ i ∈ s, √(l2NormSq (f i))

Minkowski for any finite family of scalar cell functions.

@[reducible, inline]

abbrev AVenhance.Infra.Section4.EuclideanVec2 : Type

Two-dimensional real vectors equipped with the Euclidean norm.

Equations

• AVenhance.Infra.Section4.EuclideanVec2 = PiLp 2 fun (x : Fin 2) => ℝ

def AVenhance.Infra.Section4.euclideanVec2Lift (v : Homogenization.Vec 2) : EuclideanVec2

Realize a Vec 2 field in the Euclidean L² carrier used for spacetime Minkowski estimates.

Equations

• AVenhance.Infra.Section4.euclideanVec2Lift v = WithLp.toLp 2 v

theorem AVenhance.Infra.Section4.TLemmasNorm.euclideanVec2Lift_norm_sq (v : Homogenization.Vec 2) : ‖euclideanVec2Lift v‖ ^ 2 = Homogenization.vecNormSq v

theorem AVenhance.Infra.Section4.TLemmasNorm.memLp_euclideanLift_finset_sum {ι : Type u_1} (s : Finset ι) (F : ι → ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ∀ i ∈ s, MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => euclideanVec2Lift (F i p)) 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => euclideanVec2Lift (∑ i ∈ s, F i p)) 2 (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Section4.TLemmasNorm.spaceGrad_finset_sum {ι : Type u_1} (s : Finset ι) (u : ι → ℝ → Homogenization.Vec 2 → ℝ) (hD : ∀ i ∈ s, ∀ (t : ℝ), 0 < t → Differentiable ℝ (u i t)) (t : ℝ) (ht : 0 < t) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => ∑ i ∈ s, u i t y) x = ∑ i ∈ s, spaceGrad (u i t) x