Local Energy Limit Algebra

Local energy identities and limit passages for the endpoint regularity proof.

theorem ESS.localEnergyLimitAlgebraHolderTripleFourFourTwo : ENNReal.HolderTriple 4 4 2

theorem ESS.localEnergyLimitAlgebraHolderTripleFourFourFourThirds : ENNReal.HolderTriple 2 4 (ENNReal.ofReal (4 / 3))

theorem ESS.localEnergyLimitAlgebraHolderTripleFourThirdsFourOne : (ENNReal.ofReal (4 / 3)).HolderTriple 4 1

theorem ESS.localEnergyLimitAlgebraHolderTripleThreeHalvesFourTwelveElevenths : (ENNReal.ofReal (3 / 2)).HolderTriple 4 (ENNReal.ofReal (12 / 11))

theorem ESS.localEnergyLimitAlgebraHolderTripleTwelveEleventhsTwelveOne : (ENNReal.ofReal (12 / 11)).HolderTriple 12 1

theorem ESS.localEnergyLimitAlgebraHolderTripleTwoTwoOne : ENNReal.HolderTriple 2 2 1

def ESS.localEnergyLimitSpatialDir (j : Fin 3) : CKN.Foundation.Parabolic.Vec3 × ℝ

The product-space direction corresponding to the jth spatial coordinate.

Equations

• ESS.localEnergyLimitSpatialDir j = ESS.spatialDir j

def ESS.localEnergyLimitTimeDir : CKN.Foundation.Parabolic.Vec3 × ℝ

The product-space direction corresponding to the time coordinate.

Equations

• ESS.localEnergyLimitTimeDir = ESS.timeDir

noncomputable def ESS.localEnergyLimitBaseIntegrand (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (R G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ) (p ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The unexpanded local energy density used by the smooth identity.

Equations

• ESS.localEnergyLimitBaseIntegrand u R G p ψ = ESS.smoothEnergyBaseIntegrand u R G p ψ

noncomputable def ESS.localEnergyLimitExpandedBaseIntegrand (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) (R G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ) (p : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (ψ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ

The componentwise expansion of the local energy density.

Equations

• One or more equations did not get rendered due to their size.

theorem ESS.localEnergy_smoothBase_eq_expanded {u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {R G : CKN.Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Fin 3 → ℝ} {p ψ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : localEnergyLimitBaseIntegrand u R G p ψ = localEnergyLimitExpandedBaseIntegrand u R G p (have this := ψ; this)

The smooth local energy density agrees pointwise with its componentwise expansion.

theorem ESS.localEnergy_tendsto_eLpNorm_double_sum_sub {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp : 1 ≤ p) [Fintype ι] [Fintype κ] {fn : ℕ → ι → κ → α → ℝ} {f : ι → κ → α → ℝ} (hconv : ∀ (i : ι) (j : κ), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n i j x - f i j x) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => ∑ i : ι, ∑ j : κ, fn n i j x - ∑ i : ι, ∑ j : κ, f i j x) p μ) Filter.atTop (nhds 0)

Finite double sums preserve convergence in an Lᵖ seminorm for p ≥ 1.

theorem ESS.localEnergy_tendsto_eLpNorm_mul_fixed {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q r : ENNReal} [p.HolderTriple q r] (hr : 1 ≤ r) {f g : α → ℝ} (hf : MeasureTheory.MemLp f p μ) (hg : MeasureTheory.MemLp g q μ) {fn : ℕ → α → ℝ} (hfn : ∀ (n : ℕ), MeasureTheory.MemLp (fn n) p μ) (hfnLim : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n x - f x) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n x * g x - f x * g x) r μ) Filter.atTop (nhds 0)

Multiplication by a fixed Lᵖ function preserves the corresponding Hölder convergence.

theorem ESS.localEnergy_tendsto_eLpNorm_const_smul_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} {f : α → ℝ} {fn : ℕ → α → ℝ} (c : ℝ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => fn n x - f x) p μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (x : α) => c * fn n x - c * f x) p μ) Filter.atTop (nhds 0)

Constant scalar multiplication preserves convergence in an Lᵖ seminorm.

theorem ESS.localEnergy_integral_tendsto_of_L1 {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] {μ : MeasureTheory.Measure α} {f : α → E} {fn : ℕ → α → E} (hfn : ∀ (n : ℕ), MeasureTheory.MemLp (fn n) 1 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fn n - f) 1 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), fn n x ∂μ) Filter.atTop (nhds (∫ (x : α), f x ∂μ))

L¹ convergence implies convergence of Bochner integrals.

theorem ESS.localEnergy_memLp_double_sum {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} [Fintype ι] [Fintype κ] {f : ι → κ → α → ℝ} (hf : ∀ (i : ι) (j : κ), MeasureTheory.MemLp (f i j) p μ) : MeasureTheory.MemLp (fun (x : α) => ∑ i : ι, ∑ j : κ, f i j x) p μ

A finite double sum of Lᵖ functions belongs to Lᵖ.