Genuine finite-Sobolev PDE energy passage on every time subinterval.

Exact signed Gevrey integral energy for actual finite-Sobolev viscous solutions.

theorem EulerWeightedSobolevEnergy.weighted_sobolev_energy_integral (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (hq : 3 ≤ q) (order : α → ℕ) (ρ ρ' : ℝ → ℝ) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K G : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (e : α → β → ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (e' p forcing : α → β → ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (z : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (s t c ν : ℝ) (K' : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (B : ℝ → NNReal) (hst : s ≤ t) (hc : 0 < c) (hν : 0 ≤ ν) (hρc : ContinuousOn ρ (Set.Icc s t)) (hρpos : ∀ u ∈ Set.Icc s t, 0 < ρ u) (hρd : ∀ u ∈ Set.Ioo s t, HasDerivAt ρ (ρ' u) u) (hKc : ContinuousOn (fun (u : ℝ) => (K u).operator) (Set.Icc s t)) (hec : ∀ (i : α) (j : β), ContinuousOn (fun (u : ℝ) => EulerCylinderSobolevSpace.value period (e i j u)) (Set.Icc s t)) (hKt : ∀ u ∈ Set.Ioo s t, HasDerivAt (fun (v : ℝ) => (K v).operator) (K' u) u) (het : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, HasDerivAt (fun (v : ℝ) => EulerCylinderSobolevSpace.value period (e i j v)) (e' i j u) u) (hsym : ∀ u ∈ Set.Ioo s t, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ (((K u).coefficient x) v) w = inner ℝ v (((K u).coefficient x) w)) (hpos : ∀ u ∈ Set.Icc s t, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((K u).coefficient x) v) v) (hKG : ∀ u ∈ Set.Ioo s t, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), ((K u).coefficient x) (((G u).coefficient x) v) = v) (hediv : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, EulerCylinderSobolevSpace.value period (e i j u) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hp : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, p i j u ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (hz : ∀ u ∈ Set.Ioo s t, EulerCylinderSobolevSpace.value period (z u) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hzB : ∀ u ∈ Set.Ioo s t, ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period (z u)) x‖ ≤ ↑(B u)) (heq : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, e' i j u + (EulerSobolevMetricTransport.transportOperator period hq κ m (z u)) ((EulerCylinderSobolevSpace.restrictOperator period weighted_sobolev_energy_integral._proof_1) (e i j u)) + (G u).operator (p i j u) = forcing i j u + ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period (e i j u))) (hAint : ∀ (i : α), MeasureTheory.IntegrableOn (fun (u : ℝ) => EulerPacketWeights.weight (ρ u) (order i) * EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K u) (K' u) κ m c ν (B u) + ρ' u / ρ u * ↑(order i) * EulerPacketWeights.weight (ρ u) (order i)) (Set.Icc s t) MeasureTheory.volume) (hFint : ∀ (i : α), MeasureTheory.IntegrableOn (fun (u : ℝ) => EulerPacketWeights.weight (ρ u) (order i) * (↑(K u).bound / c * EulerFiniteMetricEnergy.familyNorm fun (j : β) => forcing i j u)) (Set.Icc s t) MeasureTheory.volume) : ((EulerWeightedCylinderEnergy.weightedMetricSum (ρ t) order (K t).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j t)) - EulerWeightedCylinderEnergy.weightedMetricSum (ρ s) order (K s).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j s)) ≤ ∫ (u : ℝ) in s..t, ((EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K u) (K' u) κ m c ν (B u) * EulerWeightedCylinderEnergy.weightedMetricSum (ρ u) order (K u).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j u)) + ρ' u / ρ u * EulerWeightedCylinderEnergy.weightedMetricLoss (ρ u) order (K u).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e i j u)) + ↑(K u).bound / c * EulerWeightedCylinderEnergy.weightedForcingSum (ρ u) order fun (i : α) (j : β) => forcing i j u

The finite Gevrey-weighted integral energy inequality derived from the actual viscous PDE. The signed radius term is retained exactly, and no differentiability of the unregularized norm is assumed.

theorem EulerPDESubintervalEnergyLimit.integral_eq_three_subinterval_paths (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (hst : s ≤ t) (a b c X Y Z : C(↑(Set.Icc 0 T), ℝ)) (f : ℝ → ℝ) (hf : ∀ r ∈ Set.Icc s t, f r = EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT X r + EulerVolterraConvolution.extendPath T hT b r * EulerVolterraConvolution.extendPath T hT Y r + EulerVolterraConvolution.extendPath T hT c r * EulerVolterraConvolution.extendPath T hT Z r) : ∫ (r : ℝ) in s..t, f r = ((∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT X r) + ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT b r * EulerVolterraConvolution.extendPath T hT Y r) + ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT c r * EulerVolterraConvolution.extendPath T hT Z r

Three continuous weighted paths identify the actual scalar integral on an arbitrary time subinterval.

theorem EulerPDESubintervalEnergyLimit.weighted_pde_energy_subinterval_limit (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] {q : ℕ} (hq : 3 ≤ q) (T : ℝ) (hT : 0 ≤ T) (s t : ℝ) (h0s : 0 ≤ s) (hst : s ≤ t) (htT : t ≤ T) (order : α → ℕ) (ρ ρ' : ℝ → ℝ) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K G : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (e : ℕ → α → β → ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)) (e' p forcing : ℕ → α → β → ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (z : ℝ → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (c ν : ℝ) (K' : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (B : ℝ → NNReal) (hc : 0 < c) (hν : 0 ≤ ν) (hρc : ContinuousOn ρ (Set.Icc 0 T)) (hρpos : ∀ r ∈ Set.Icc 0 T, 0 < ρ r) (hρd : ∀ r ∈ Set.Ioo 0 T, HasDerivAt ρ (ρ' r) r) (hKc : ContinuousOn (fun (r : ℝ) => (K r).operator) (Set.Icc 0 T)) (hec : ∀ (n : ℕ) (i : α) (j : β), ContinuousOn (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (e n i j r)) (Set.Icc 0 T)) (hKt : ∀ r ∈ Set.Ioo 0 T, HasDerivAt (fun (v : ℝ) => (K v).operator) (K' r) r) (het : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, HasDerivAt (fun (v : ℝ) => EulerCylinderSobolevSpace.value period (e n i j v)) (e' n i j r) r) (hsym : ∀ r ∈ Set.Ioo 0 T, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v w : EulerLiftedGradientSpace.Vector3), inner ℝ (((K r).coefficient x) v) w = inner ℝ v (((K r).coefficient x) w)) (hpos : ∀ r ∈ Set.Icc 0 T, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (((K r).coefficient x) v) v) (hKG : ∀ r ∈ Set.Ioo 0 T, ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), ((K r).coefficient x) (((G r).coefficient x) v) = v) (hediv : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, EulerCylinderSobolevSpace.value period (e n i j r) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hp : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, p n i j r ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (hz : ∀ r ∈ Set.Ioo 0 T, EulerCylinderSobolevSpace.value period (z r) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hzB : ∀ r ∈ Set.Ioo 0 T, ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period (z r)) x‖ ≤ ↑(B r)) (heq : ∀ (n : ℕ) (i : α) (j : β), ∀ r ∈ Set.Ioo 0 T, e' n i j r + (EulerSobolevMetricTransport.transportOperator period hq κ m (z r)) ((EulerCylinderSobolevSpace.restrictOperator period EulerWeightedSobolevEnergy.weighted_sobolev_energy_integral._proof_1) (e n i j r)) + (G r).operator (p n i j r) = forcing n i j r + ν • EulerMetricHeatEnergy.jetLaplacian period (EulerCylinderSobolevSpace.toJet period (e n i j r))) (hAint : ∀ (i : α), MeasureTheory.IntegrableOn (fun (r : ℝ) => EulerPacketWeights.weight (ρ r) (order i) * EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K r) (K' r) κ m c ν (B r) + ρ' r / ρ r * ↑(order i) * EulerPacketWeights.weight (ρ r) (order i)) (Set.Icc 0 T) MeasureTheory.volume) (hFint : ∀ (n : ℕ) (i : α), MeasureTheory.IntegrableOn (fun (r : ℝ) => EulerPacketWeights.weight (ρ r) (order i) * (↑(K r).bound / c * EulerFiniteMetricEnergy.familyNorm fun (j : β) => forcing n i j r)) (Set.Icc 0 T) MeasureTheory.volume) (a b d : C(↑(Set.Icc 0 T), ℝ)) (ha : ∀ r ∈ Set.Icc 0 T, EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K r) (K' r) κ m c ν (B r) = EulerVolterraConvolution.extendPath T hT a r) (hb : ∀ r ∈ Set.Icc 0 T, ρ' r / ρ r = EulerVolterraConvolution.extendPath T hT b r) (hd : ∀ r ∈ Set.Icc 0 T, ↑(K r).bound / c = EulerVolterraConvolution.extendPath T hT d r) (X Y Z : ℕ → C(↑(Set.Icc 0 T), ℝ)) (hXdef : ∀ (n : ℕ), ∀ r ∈ Set.Icc 0 T, (EulerWeightedCylinderEnergy.weightedMetricSum (ρ r) order (K r).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e n i j r)) = EulerVolterraConvolution.extendPath T hT (X n) r) (hYdef : ∀ (n : ℕ), ∀ r ∈ Set.Icc 0 T, (EulerWeightedCylinderEnergy.weightedMetricLoss (ρ r) order (K r).operator fun (i : α) (j : β) => EulerCylinderSobolevSpace.value period (e n i j r)) = EulerVolterraConvolution.extendPath T hT (Y n) r) (hZdef : ∀ (n : ℕ), ∀ r ∈ Set.Icc 0 T, (EulerWeightedCylinderEnergy.weightedForcingSum (ρ r) order fun (i : α) (j : β) => forcing n i j r) = EulerVolterraConvolution.extendPath T hT (Z n) r) (x y : C(↑(Set.Icc 0 T), ℝ)) (f : ↥(EulerTimeLp.TimeLp T ℝ)) (hX : Filter.Tendsto X Filter.atTop (nhds x)) (hY : Filter.Tendsto Y Filter.atTop (nhds y)) (hZ : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (Z n)) Filter.atTop (nhds f)) : x ⟨t, ⋯⟩ - x ⟨s, ⋯⟩ ≤ ((∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT a r * EulerVolterraConvolution.extendPath T hT x r) + ∫ (r : ℝ) in s..t, EulerVolterraConvolution.extendPath T hT b r * EulerVolterraConvolution.extendPath T hT y r) + ∫ (r : ℝ) in Set.Icc s t, ↑↑(EulerTimeLp.pathLp T hT d) r * ↑↑f r ∂EulerTimeLp.timeMeasure T

Actual smooth-in-time finite-Sobolev PDE approximations imply the limiting signed integral energy bound. The premises include their literal PDEs and strong convergence, never an assumed energy inequality.