Actual Gevrey-weighted cylinder energy with signed radius derivative and no zero-norm differentiation.

noncomputable def EulerWeightedCylinderEnergy.weightedMetricSum {α : Type u_1} {β : Type u_2} {H : Type u_3} [Fintype α] [Fintype β] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ) (order : α → ℕ) (K : H →L[ℝ] H) (e : α → β → H) : ℝ

The finite external-word Gevrey sum of the source's base-word metric roots.

Equations

• EulerWeightedCylinderEnergy.weightedMetricSum ρ order K e = ∑ i : α, EulerPacketWeights.weight ρ (order i) * EulerFiniteMetricEnergy.familyMetricNorm K (e i)

noncomputable def EulerWeightedCylinderEnergy.weightedMetricLoss {α : Type u_1} {β : Type u_2} {H : Type u_3} [Fintype α] [Fintype β] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ) (order : α → ℕ) (K : H →L[ℝ] H) (e : α → β → H) : ℝ

The same metric sum with the external derivative count, giving the radius-loss term.

Equations

• EulerWeightedCylinderEnergy.weightedMetricLoss ρ order K e = ∑ i : α, ↑(order i) * EulerPacketWeights.weight ρ (order i) * EulerFiniteMetricEnergy.familyMetricNorm K (e i)

noncomputable def EulerWeightedCylinderEnergy.weightedForcingSum {α : Type u_1} {β : Type u_2} {H : Type u_3} [Fintype α] [Fintype β] [NormedAddCommGroup H] (ρ : ℝ) (order : α → ℕ) (f : α → β → H) : ℝ

The actual finite weighted sum of base-word Hilbert forcing norms.

Equations

• EulerWeightedCylinderEnergy.weightedForcingSum ρ order f = ∑ i : α, EulerPacketWeights.weight ρ (order i) * EulerFiniteMetricEnergy.familyNorm (f i)

noncomputable def EulerWeightedCylinderEnergy.viscousGrowthCoefficient (period : ℝ) [Fact (0 < period)] (K : EulerSpatialSobolevInverse.SmoothCoefficient period) (K' : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c ν : ℝ) (B : NNReal) : ℝ

The explicit common coefficient in the actual viscous metric-root estimate.

Equations

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

theorem EulerWeightedCylinderEnergy.weighted_cylinder_energy_integral (period : ℝ) [Fact (0 < period)] {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (order : α → ℕ) (ρ ρ' : ℝ → ℝ) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (K G : ℝ → EulerSpatialSobolevInverse.SmoothCoefficient period) (e e' p forcing : α → β → ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (z : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (s t c ν : ℝ) (K' : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (B : ℝ → NNReal) (J : (i : α) → (j : β) → (u : ℝ) → u ∈ Set.Ioo s t → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 2 (e i j u)) (g : α → β → ℝ → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hrep : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, ↑↑(e i j u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g i j u) (hg : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (g i j u) x)) (hDg : ∀ (i : α) (j : β), ∀ u ∈ Set.Ioo s t, MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.LiftDomain period) => fderiv ℝ (EulerMetricTransport.localFieldLift period (g i j u) x) 0) 2 (EulerLiftedGradientSpace.liftMeasure period)) (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 (e i j) (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 (e i j) (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, 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, z u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hzB : ∀ u ∈ Set.Ioo s t, ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(z u) x‖ ≤ ↑(B u)) (heq : ∀ (i : α) (j : β) (u : ℝ) (hu : u ∈ Set.Ioo s t), e' i j u + EulerRepresentativeMetricEvolution.liftedTransport period κ m (g i j u) (z u) ⋯ (B u) ⋯ + (G u).operator (p i j u) = forcing i j u + ν • EulerMetricHeatEnergy.jetLaplacian period (J i j u hu)) (hAint : ∀ (i : α), MeasureTheory.IntegrableOn (fun (u : ℝ) => EulerPacketWeights.weight (ρ u) (order i) * 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) : ((weightedMetricSum (ρ t) order (K t).operator fun (i : α) (j : β) => e i j t) - weightedMetricSum (ρ s) order (K s).operator fun (i : α) (j : β) => e i j s) ≤ ∫ (u : ℝ) in s..t, ((viscousGrowthCoefficient period (K u) (K' u) κ m c ν (B u) * weightedMetricSum (ρ u) order (K u).operator fun (i : α) (j : β) => e i j u) + ρ' u / ρ u * weightedMetricLoss (ρ u) order (K u).operator fun (i : α) (j : β) => e i j u) + ↑(K u).bound / c * 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.