Continuous scalar majorants derived from actual coefficient budgets and actual nonlinear time fields.

theorem EulerCorrectionEnergyMajorants.energy_nonneg (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (t : ↑(Set.Icc 0 T)) : 0 ≤ (EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t

Actual metric energy is nonnegative along every positive-radius solution path.

theorem EulerCorrectionEnergyMajorants.loss_nonneg (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (t : ↑(Set.Icc 0 T)) : 0 ≤ (EulerEnergyMetricPaths.lossPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t

Actual metric radius loss is nonnegative along the same solution path.

theorem EulerCorrectionEnergyMajorants.velocity_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (t : ↑(Set.Icc 0 T)) : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ‖↑↑(EulerCylinderSobolevSpace.value period ((EulerCorrectionEnergyTime.velocityPath period D e) t)) x‖ ≤ ↑(EulerGevreyMetricEstimate.metricVelocityBound period K.c S.B0 ((EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t))

The actual total velocity has the genuine metric-energy pointwise bound.

theorem EulerCorrectionEnergyMajorants.velocity_divergenceFree (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (he : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (e t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (t : ↑(Set.Icc 0 T)) : EulerCylinderSobolevSpace.value period ((EulerCorrectionEnergyTime.velocityPath period D e) t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction

Adding the actual divergence-free approximation and error preserves the lifted constraint.

noncomputable def EulerCorrectionEnergyMajorants.growthPath (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : C(↑(Set.Icc 0 T), ℝ)

The fixed affine continuous majorant of actual metric growth.

Equations

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

noncomputable def EulerCorrectionEnergyMajorants.radiusLossPath {T : ℝ} (R Rdot : C(↑(Set.Icc 0 T), ℝ)) (hR : ∀ (t : ↑(Set.Icc 0 T)), 0 < R t) : C(↑(Set.Icc 0 T), ℝ)

The signed radius derivative divided by the actual positive radius.

Equations

• EulerCorrectionEnergyMajorants.radiusLossPath R Rdot hR = { toFun := fun (t : ↑(Set.Icc 0 T)) => Rdot t / R t, continuous_toFun := ⋯ }

noncomputable def EulerCorrectionEnergyMajorants.forcingMajorant (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : C(↑(Set.Icc 0 T), ℝ)

The literal continuous nonlinear forcing majorant.

Equations

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

theorem EulerCorrectionEnergyMajorants.growthPath_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (ν : ℝ) (hν : ν ≤ 1) (t : ↑(Set.Icc 0 T)) : EulerWeightedCylinderEnergy.viscousGrowthCoefficient period (K.metric t) (K.derivative t) D.κ D.direction K.c ν (EulerGevreyMetricEstimate.metricVelocityBound period K.c S.B0 ((EulerEnergyMetricPaths.energyPath period N hN T R (EulerCorrectionEnergyData.MetricBudget.operatorPath period K) e) t)) ≤ (growthPath period S hN K e) t

The actual metric-growth coefficient is bounded by the continuous affine majorant.

theorem EulerCorrectionEnergyMajorants.forcingMajorant_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) (hN : N + 6 ≤ q + 1) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) (hG : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n e)) Filter.atTop (nhds U)) : ↑↑(EulerCorrectionEnergyTime.weightedCorrectionForcing period hq T hT D hG N hN R e U) ≤ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (forcingMajorant period S hN K e)

The actual full-order nonlinear forcing has the continuous majorant derived from its genuine coefficient budgets.

noncomputable def EulerCorrectionEnergyMajorants.combinedConstant (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) : ℝ

The explicit cutoff-independent constant in the scalar shrinking-radius estimate.

Equations

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

theorem EulerCorrectionEnergyMajorants.combinedConstant_pos (period : ℝ) [Fact (0 < period)] {q : ℕ} {T : ℝ} {hq : 6 ≤ q + 1} {D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)} {N : ℕ} {R : C(↑(Set.Icc 0 T), ℝ)} (S : EulerCorrectionEnergyData.SpatialBudget period hq D N R) {hT : 0 ≤ T} (K : EulerCorrectionEnergyData.MetricBudget period T hT D) : 0 < combinedConstant period S K

The actual combined constant is strictly positive.