One explicit cutoff-independent scalar constant absorbs the actual metric growth and nonlinear forcing coefficients.

The actual nonlinear Bochner forcing is bounded by a continuous metric-energy polynomial, with constants independent of the external cutoff.

The actual complete Euler forcing estimate in metric-energy variables.

theorem EulerGevreyMetricEstimate.correctionForcing_metric (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (KG : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (KG0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (N : ℕ) (hN : N + 6 ≤ s) (ρ Rc M B : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hB : 0 ≤ B) (hbase5 : (EulerH6Pressure.CoefficientJet.restrict KG 5 ⋯).pressureConstant c ≤ M) (hbase6 : (EulerH6Pressure.CoefficientJet.restrict KG 6 hs).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period KG 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (hG : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period KG r ≤ B) (hG0 : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period KG0 r ≤ B) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (C0 : EulerSpatialSobolevInverse.SmoothCoefficient period) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s C0) (C : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s (C i)) (z e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (r : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (B0 B1 A0 A2 R : ℝ) (hA2 : 0 ≤ A2) (hz : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ z ≤ B0) (hdz : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N ρ ((EulerCylinderSobolevSpace.derivativeOperator period s i) z) ≤ B1) (hC0 : EulerSobolevGevreyOperators.weightedCoefficient period K0 6 N ρ ≤ A0) (hC : ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period (K i) 6 N ρ ≤ A2) (hr : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ r ≤ R) (KM : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (cM : ℝ) (hcM : 0 < cM) (hKM : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), cM ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (KM v) v) : have f := EulerGevreyOrderZero.orderZeroSource period hs L hL (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K0) (fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) z r ((EulerCylinderSobolevSpace.truncateOperator period s) e); EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (EulerGevreyCorrectionForcing.correctionForcing period hs KG KG0 N hN L hL (z + e) e f ((EulerSobolevCoefficientPressure.pressureSobolevOperator period KG κ m c hc hpos) f) (EulerGevreyPressureTransport.transportPressure period hs KG κ m c hc hpos L hL (z + e) e)) ≤ EulerGevreyCorrectionBound.sourceConstant B M * R + (EulerGevreyCorrectionBound.sourceConstant B M * (EulerH6Nonlinear.productConstant period 3 * B1 + A0 + 2 * A2 * EulerH6Nonlinear.productConstant period 3 * B0) + EulerGevreyCorrectionBound.transportConstant period B M * B0) * metricAmplification cM * energyNorm period N ⋯ ρ KM e + (EulerGevreyCorrectionBound.sourceConstant B M * A2 * EulerH6Nonlinear.productConstant period 3 + EulerGevreyCorrectionBound.transportConstant period B M) * metricAmplification cM ^ 2 * energyNorm period N ⋯ ρ KM e ^ 2 + EulerGevreyCorrectionBound.lossConstant period M * (ρ⁻¹ + Rc) * metricAmplification cM ^ 2 * (B0 + energyNorm period N ⋯ ρ KM e) * energyLoss period N ⋯ ρ KM e

The complete actual correction forcing has the metric polynomial bound used in the shrinking-radius energy argument.

@[instance_reducible]

noncomputable def EulerCorrectionEnergyBound.boundTimeGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

A local concrete normed-group instance for the actual Sobolev energy scale.

Equations

• EulerCorrectionEnergyBound.boundTimeGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerCorrectionEnergyBound.boundTimeSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

A local concrete real normed-space instance for the actual Sobolev energy scale.

Equations

• EulerCorrectionEnergyBound.boundTimeSpace period q = inferInstance

noncomputable def EulerCorrectionEnergyBound.forcingPolynomial (period : ℝ) [Fact (0 < period)] (B M B0 B1 A0 A2 residual cM Rc ρ X Y : ℝ) : ℝ

The explicit scalar majorant for the genuine seven-term nonlinear metric forcing.

Equations

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

theorem EulerCorrectionEnergyBound.correctionArray_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q + 1) {T : ℝ} (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (K6 : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 (D.metric.coefficient t)) (N : ℕ) (hN : N + 6 ≤ q + 1) (τ : ↑(Set.Icc 0 T)) (ρ Rc M B : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hB : 0 ≤ B) (hbase5 : (EulerH6Pressure.CoefficientJet.restrict (D.metric.jet τ) 5 ⋯).pressureConstant D.coercivity ≤ M) (hbase6 : (EulerH6Pressure.CoefficientJet.restrict (D.metric.jet τ) 6 hq).pressureConstant D.coercivity ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period (D.metric.jet τ) 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (hG : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period (D.metric.jet τ) r ≤ B) (hG0 : ∀ r ≤ 6, EulerJetProductBounds.boundLevel period (K6 τ) r ≤ B) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (V : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1))) (hV : (EulerCylinderSobolevSpace.truncateOperator period (q + 1)) V = e τ) (B0 B1 A0 A2 residual : ℝ) (hA2 : 0 ≤ A2) (hz : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ (D.approximation τ) ≤ B0) (hdz : ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N ρ ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) (D.approximation τ)) ≤ B1) (hC0 : EulerSobolevGevreyOperators.weightedCoefficient period (D.linear.jet τ) 6 N ρ ≤ A0) (hC : ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period ((D.quadratic i).jet τ) 6 N ρ ≤ A2) (hr : EulerSobolevGevreyOperators.weightedNorm period 6 N ρ (D.residual τ) ≤ residual) (KM : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (cM : ℝ) (hcM : 0 < cM) (hKM : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), cM ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (KM v) v) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (EulerCorrectionEnergyTime.correctionArray period hq D K6 N hN e V τ) ≤ forcingPolynomial period B M B0 B1 A0 A2 residual cM Rc ρ (EulerGevreyMetricEstimate.energyNorm period N ⋯ ρ KM V) (EulerGevreyMetricEstimate.energyLoss period N ⋯ ρ KM V)

The literal spatial correction array has the actual metric polynomial bound for every valid higher representative.

noncomputable def EulerCorrectionEnergyBound.forcingBoundPath (period : ℝ) [Fact (0 < period)] {q : ℕ} (N : ℕ) (hN : N + 6 ≤ q + 1) (T : ℝ) (R : C(↑(Set.Icc 0 T), ℝ)) (hR : ∀ (t : ↑(Set.Icc 0 T)), 0 < R t) (K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (B M B0 B1 A0 A2 residual cM Rc : ℝ) : C(↑(Set.Icc 0 T), ℝ)

The literal polynomial majorant is continuous along the positive radius and actual continuous metric energies.

Equations

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

theorem EulerCorrectionEnergyBound.weightedCorrectionForcing_bound (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q + 1) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T)) (hGc : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator) (K6 : (t : ↑(Set.Icc 0 T)) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 (D.metric.coefficient t)) (N : ℕ) (hN : N + 6 ≤ q + 1) (R : C(↑(Set.Icc 0 T), ℝ)) (hR : ∀ (t : ↑(Set.Icc 0 T)), 0 < R t) (Rc M B : ℝ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hB : 0 ≤ B) (hbase5 : ∀ (t : ↑(Set.Icc 0 T)), (EulerH6Pressure.CoefficientJet.restrict (D.metric.jet t) 5 ⋯).pressureConstant D.coercivity ≤ M) (hbase6 : ∀ (t : ↑(Set.Icc 0 T)), (EulerH6Pressure.CoefficientJet.restrict (D.metric.jet t) 6 hq).pressureConstant D.coercivity ≤ M) (hsmall : ∀ (t : ↑(Set.Icc 0 T)), 4 * M * (R t * Rc) ≤ 1) (hcoeff : ∀ (t : ↑(Set.Icc 0 T)) (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period (D.metric.jet t) 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (hG : ∀ (t : ↑(Set.Icc 0 T)), ∀ r ≤ 6, EulerJetProductBounds.boundLevel period (D.metric.jet t) r ≤ B) (hG0 : ∀ (t : ↑(Set.Icc 0 T)), ∀ r ≤ 6, EulerJetProductBounds.boundLevel period (K6 t) r ≤ B) (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)) (B0 B1 A0 A2 residual : ℝ) (hA2 : 0 ≤ A2) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm period 6 N (R t) (D.approximation t) ≤ B0) (hdz : ∀ (t : ↑(Set.Icc 0 T)), ∑ i : Fin 4, EulerSobolevGevreyOperators.weightedNorm period 6 N (R t) ((EulerCylinderSobolevSpace.derivativeOperator period (q + 1) i) (D.approximation t)) ≤ B1) (hC0 : ∀ (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedCoefficient period (D.linear.jet t) 6 N (R t) ≤ A0) (hC : ∀ (t : ↑(Set.Icc 0 T)), ∑ i : Fin 3, EulerSobolevGevreyOperators.weightedCoefficient period ((D.quadratic i).jet t) 6 N (R t) ≤ A2) (hr : ∀ (t : ↑(Set.Icc 0 T)), EulerSobolevGevreyOperators.weightedNorm period 6 N (R t) (D.residual t) ≤ residual) (K : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period))) (cM : ℝ) (hcM : 0 < cM) (hKM : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), cM ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ ((K t) v) v) : ↑↑(EulerCorrectionEnergyTime.weightedCorrectionForcing period hq T hT D hGc N hN R e U) ≤ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT (forcingBoundPath period N hN T R hR K e B M B0 B1 A0 A2 residual cM Rc)

The actual constructed full-order Bochner forcing obeys the continuous spatial majorant almost everywhere.

noncomputable def EulerNonlinearEnergyConstants.linearCoefficient (period : ℝ) [Fact (0 < period)] (B M B0 B1 A0 A2 c : ℝ) : ℝ

The fixed coefficient of the metric-linear part of the actual nonlinear forcing.

Equations

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

noncomputable def EulerNonlinearEnergyConstants.quadraticCoefficient (period : ℝ) [Fact (0 < period)] (B M A2 c : ℝ) : ℝ

The fixed coefficient of the metric-quadratic part of the actual nonlinear forcing.

Equations

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

noncomputable def EulerNonlinearEnergyConstants.lossCoefficient (period : ℝ) [Fact (0 < period)] (M c : ℝ) : ℝ

The fixed coefficient of the single derivative-loss factor in the actual nonlinear forcing.

Equations

• EulerNonlinearEnergyConstants.lossCoefficient period M c = EulerGevreyCorrectionBound.lossConstant period M * EulerGevreyMetricEstimate.metricAmplification c ^ 2

noncomputable def EulerNonlinearEnergyConstants.energyConstant (period : ℝ) [Fact (0 < period)] (g0 g1 k B M B0 B1 A0 A2 c : ℝ) : ℝ

One explicit constant independent of the external cutoff controls all actual scalar energy coefficients.

Equations

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

theorem EulerNonlinearEnergyConstants.coefficients_nonneg (period : ℝ) [Fact (0 < period)] (B M B0 B1 A0 A2 c : ℝ) (hB : 0 ≤ B) (hM : 0 ≤ M) (hB0 : 0 ≤ B0) (hB1 : 0 ≤ B1) (hA0 : 0 ≤ A0) (hA2 : 0 ≤ A2) (hc : 0 < c) : 0 ≤ linearCoefficient period B M B0 B1 A0 A2 c ∧ 0 ≤ quadraticCoefficient period B M A2 c ∧ 0 ≤ lossCoefficient period M c

The three actual nonlinear forcing coefficients are nonnegative under their genuine norm budgets.

theorem EulerNonlinearEnergyConstants.energyConstant_pos (period : ℝ) [Fact (0 < period)] (g0 g1 k B M B0 B1 A0 A2 c : ℝ) (hg0 : 0 ≤ g0) (hg1 : 0 ≤ g1) (hk : 0 ≤ k) (hB : 0 ≤ B) (hM : 0 ≤ M) (hB0 : 0 ≤ B0) (hB1 : 0 ≤ B1) (hA0 : 0 ≤ A0) (hA2 : 0 ≤ A2) (hc : 0 < c) : 0 < energyConstant period g0 g1 k B M B0 B1 A0 A2 c

The actual combined energy constant is strictly positive.

theorem EulerNonlinearEnergyConstants.actual_scalar_bound (period : ℝ) [Fact (0 < period)] (g0 g1 k B M B0 B1 A0 A2 c Rc ρ residual X Y b : ℝ) (hg0 : 0 ≤ g0) (hg1 : 0 ≤ g1) (hk : 0 ≤ k) (hB : 0 ≤ B) (hM : 0 ≤ M) (hB0 : 0 ≤ B0) (hB1 : 0 ≤ B1) (hA0 : 0 ≤ A0) (hA2 : 0 ≤ A2) (hc : 0 < c) (hRc : 0 ≤ Rc) (hρ : 0 < ρ) (hr : 0 ≤ residual) (hX : 0 ≤ X) (hY : 0 ≤ Y) : have C := energyConstant period g0 g1 k B M B0 B1 A0 A2 c; (g0 + g1 * X) * X + b * Y + k * EulerCorrectionEnergyBound.forcingPolynomial period B M B0 B1 A0 A2 residual c Rc ρ X Y ≤ C * (X + X ^ 2 + residual) + (b + C * (ρ⁻¹ + Rc) * (B0 + X)) * Y

The actual polynomial energy right-hand side has precisely the source's shrinking-radius form with the explicit constant.