Constructed nonlinear time fields and their exact full-order metric forcing for the Euler correction.
Exact energy forcing from the literal raw, projected, and signed-pressure field identities.
Actual coercive projected sources have precisely the signed energy forcing required by the differentiated equation.
theorem
EulerProjectedEnergyForcing.projected_negative_split
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s 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)
(T F : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
-(EulerSobolevCoefficientPressure.projectedSourceOperator period K κ m c hc hpos) (T + F) = -(T + F - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K)
((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) F) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K)
((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) T))
The actual pressure-projected negative source splits into its two positive pressure solves with the literal PDE signs.
theorem
EulerProjectedEnergyForcing.pressure_negative_split
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s 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)
(T F : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
:
-(EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) (T + F) = -((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) F + (EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) T)
The signed actual pressure is the negative sum of the two genuine component pressure solves.
theorem
EulerProjectedEnergyForcing.projected_forcing_word
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
(hs : 6 ≤ s)
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A)
(K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A)
(N : ℕ)
(hN : N + 6 ≤ s)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v)
(hL : ∀ (i : Fin 4), ‖EulerSobolevTransport.velocityComponents κ m i‖ ≤ 1)
(z : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))
(hzu : EulerCylinderSobolevSpace.value period z = EulerCylinderSobolevSpace.value period u)
(f : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
(I : EulerGevreyMetricComparison.ExternalWord N)
(a : EulerBaseWordMetric.BaseWord 6)
:
EulerCylinderSobolevSpace.word period
(-(EulerSobolevCoefficientPressure.projectedSourceOperator period K κ m c hc hpos)
(((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents κ m) hL) u)
v + f))
⋯ (EulerEnergyWordCoordinates.energyWord I a) + (EulerSobolevMetricTransport.transportOperator period ⋯ κ m z)
((EulerMildTopWord.boundedWordBlock period 1 (EulerEnergyWordCoordinates.energyLength I a) ⋯
(EulerEnergyWordCoordinates.energyWord I a))
v) + A.operator
(EulerCylinderSobolevSpace.word period
(-(EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos)
(((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents κ m) hL) u)
v + f))
⋯ (EulerEnergyWordCoordinates.energyWord I a)) = EulerGevreyCorrectionForcing.correctionForcing period hs K K0 N hN (EulerSobolevTransport.velocityComponents κ m) hL u
v f ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) f)
((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos)
(((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents κ m) hL) u) v))
I a
The actual coercive projected source and actual signed pressure give exactly the seven differentiated correction terms.
theorem
EulerProjectedForcingFields.forcing_word_of_actual_fields
(period : ℝ)
[Fact (0 < period)]
{s r : ℕ}
(hs : 6 ≤ s)
{A : EulerSpatialSobolevInverse.SmoothCoefficient period}
(K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A)
(K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A)
(N : ℕ)
(hN : N + 6 ≤ s)
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(c : ℝ)
(hc : 0 < c)
(hpos :
∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3),
c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v)
(hL : ∀ (i : Fin 4), ‖EulerSobolevTransport.velocityComponents κ m i‖ ≤ 1)
(z : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
(u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1)))
(V : ↥(EulerCylinderSobolevSpace.SobolevSpace period r))
(hzu : EulerCylinderSobolevSpace.value period z = EulerCylinderSobolevSpace.value period u)
(hV : EulerCylinderSobolevSpace.value period V = EulerCylinderSobolevSpace.value period v)
(f raw F P : ↥(EulerCylinderSobolevSpace.SobolevSpace period s))
(hraw :
raw = ((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents κ m) hL) u) v + f)
(hF : F = -(EulerSobolevCoefficientPressure.projectedSourceOperator period K κ m c hc hpos) raw)
(hP : P = -(EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) raw)
(I : EulerGevreyMetricComparison.ExternalWord N)
(a : EulerBaseWordMetric.BaseWord 6)
(horder : 1 + EulerEnergyWordCoordinates.energyLength I a ≤ r)
:
EulerCylinderSobolevSpace.word period F ⋯ (EulerEnergyWordCoordinates.energyWord I a) + (EulerSobolevMetricTransport.transportOperator period ⋯ κ m z)
((EulerMildTopWord.boundedWordBlock period 1 (EulerEnergyWordCoordinates.energyLength I a) horder
(EulerEnergyWordCoordinates.energyWord I a))
V) + A.operator (EulerCylinderSobolevSpace.word period P ⋯ (EulerEnergyWordCoordinates.energyWord I a)) = EulerGevreyCorrectionForcing.correctionForcing period hs K K0 N hN (EulerSobolevTransport.velocityComponents κ m) hL u
v f ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) f)
((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos)
(((EulerSobolevTransport.transportBilinear period hs (EulerSobolevTransport.velocityComponents κ m) hL) u) v))
I a
Actual raw-source and pressure identities determine the complete differentiated forcing, independently of the chosen equivalent higher representative.
Literal almost-everywhere representatives of the limiting actual word forcing.
Actual representatives of linear source, transport, and pressure combinations in Bochner time spaces.
theorem
EulerTimeLp.timeLinearForcing_ae
{E : Type u_1}
{V : Type u_2}
{W : Type u_3}
{H : Type u_4}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
(T : ℝ)
(hT : 0 ≤ T)
(D : E →L[ℝ] H)
(B : V →L[ℝ] W)
(A : C(↑(Set.Icc 0 T), W →L[ℝ] H))
(G : C(↑(Set.Icc 0 T), H →L[ℝ] H))
(U : ↥(TimeLp T V))
(F P : ↥(TimeLp T E))
:
↑↑((ContinuousLinearMap.compLpL 2 (timeMeasure T) D) F + (timeMultiplier T hT A) ((ContinuousLinearMap.compLpL 2 (timeMeasure T) B) U) + (timeMultiplier T hT G) ((ContinuousLinearMap.compLpL 2 (timeMeasure T) D) P)) =ᵐ[timeMeasure T] fun (t : ℝ) => D (↑↑F t) + (A (Set.projIcc 0 T hT t)) (B (↑↑U t)) + (G (Set.projIcc 0 T hT t)) (D (↑↑P t))
A genuine sum of fixed spatial and time-dependent operator actions has its literal pointwise representative.
theorem
EulerRegularizedForcingRepresentative.forcingWordTime_ae
(period : ℝ)
[Fact (0 < period)]
{q m : ℕ}
(hm : m ≤ q + 1)
(w : Fin m → Fin 4)
(T : ℝ)
(hT : 0 ≤ T)
(A :
C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
(F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
↑↑(EulerRegularizedForcingWord.forcingWordTime period hm w T hT A G U F P) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) =>
EulerCylinderSobolevSpace.word period (↑↑F t) hm w + (A (Set.projIcc 0 T hT t)) ((EulerMildTopWord.boundedWordBlock period 1 m ⋯ w) (↑↑U t)) + (G (Set.projIcc 0 T hT t)) (EulerCylinderSobolevSpace.word period (↑↑P t) hm w)
The limiting word forcing has exactly the differentiated-source plus transport plus pressure representative.
theorem
EulerRegularizedForcingRepresentative.forcingFamilyTime_ae
(period : ℝ)
[Fact (0 < period)]
{α : Type u_1}
{β : Type u_2}
[Fintype β]
{q : ℕ}
(d : α → β → ℕ)
(w : (i : α) → (j : β) → Fin (d i j) → Fin 4)
(hd : ∀ (i : α) (j : β), d i j ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(A :
C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
(F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(i : α)
:
↑↑(EulerRegularizedEnergyFamily.forcingFamilyTime period d w hd T hT A G U F P i) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) (j : β) =>
EulerCylinderSobolevSpace.word period (↑↑F t) ⋯ (w i j) + (A (Set.projIcc 0 T hT t)) ((EulerMildTopWord.boundedWordBlock period 1 (d i j) ⋯ (w i j)) (↑↑U t)) + (G (Set.projIcc 0 T hT t)) (EulerCylinderSobolevSpace.word period (↑↑P t) ⋯ (w i j))
The limiting finite family has its literal actual word forcing at every component almost everywhere.
theorem
EulerRegularizedForcingRepresentative.weighted_forcing_ae
(period : ℝ)
[Fact (0 < period)]
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Fintype β]
{q : ℕ}
(d : α → β → ℕ)
(w : (i : α) → (j : β) → Fin (d i j) → Fin 4)
(hd : ∀ (i : α) (j : β), d i j ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(weights : α → C(↑(Set.Icc 0 T), ℝ))
(A :
C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(G : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
(F P : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
↑↑(EulerWeightedForcingTime.weightedForcingTime T hT weights
(EulerRegularizedEnergyFamily.forcingFamilyTime period d w hd T hT A G U F P)) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) =>
∑ i : α,
EulerVolterraConvolution.extendPath T hT (weights i) t * EulerFiniteMetricEnergy.familyNorm fun (j : β) =>
EulerCylinderSobolevSpace.word period (↑↑F t) ⋯ (w i j) + (A (Set.projIcc 0 T hT t)) ((EulerMildTopWord.boundedWordBlock period 1 (d i j) ⋯ (w i j)) (↑↑U t)) + (G (Set.projIcc 0 T hT t)) (EulerCylinderSobolevSpace.word period (↑↑P t) ⋯ (w i j))
The limiting weighted forcing is the genuine finite sum of norms of the literal differentiated PDE forcing.
The constructed Bochner correction source is literally the higher-order nonlinear correction almost everywhere.
theorem
EulerTimeCorrectionStrongIdentity.rawSourceTime_transport_ae
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
(hs : 6 ≤ s)
(T : ℝ)
(hT : 0 ≤ T)
(L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ)
(hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1)
(C0 :
C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)))
(C :
Fin 3 →
C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period s)))
(z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))))
(r e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s)))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))))
(hU :
(fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period s) (↑↑U t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT e)
:
↑↑(EulerTimeCorrectionSource.rawSourceTime period hs T hT L hL C0 C z r e U) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) =>
((EulerSobolevTransport.transportBilinear period hs L hL) (EulerVolterraConvolution.extendPath T hT z t + ↑↑U t))
(↑↑U t) + EulerVolterraConvolution.extendPath T hT (EulerTimeCorrectionSource.orderZeroPath period hs T L hL C0 C z r e) t
The genuine raw source is the literal transport of the actual higher-order representative plus the prescribed lower-order terms.
theorem
EulerTimeCorrectionStrongIdentity.transport_velocity_value_ae
(period : ℝ)
[Fact (0 < period)]
{s : ℕ}
(T : ℝ)
(hT : 0 ≤ T)
(z : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period s)))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))))
(hU :
(fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period s) (↑↑U t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT e)
:
(fun (t : ℝ) =>
EulerCylinderSobolevSpace.value period
((EulerCylinderSobolevSpace.truncateOperator period s) (EulerVolterraConvolution.extendPath T hT z t) + EulerVolterraConvolution.extendPath T hT e t)) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT z t + ↑↑U t)
The continuous transport velocity and its higher Sobolev representative have the same actual L² value almost everywhere.
@[instance_reducible]
noncomputable def
EulerCorrectionEnergyTime.correctionTimeGroup
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
A local concrete normed-group instance for the actual cylinder Sobolev scale.
Equations
Instances For
@[instance_reducible]
noncomputable def
EulerCorrectionEnergyTime.correctionTimeSpace
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
:
NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)
A local concrete real normed-space instance for the actual cylinder Sobolev scale.
Equations
Instances For
noncomputable def
EulerCorrectionEnergyTime.velocityPath
(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))))
:
The actual continuous background-plus-error velocity at the energy level.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionEnergyTime.lowerOrderPath
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q + 1)
{T : ℝ}
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The actual continuous order-zero source along the original energy-level solution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionEnergyTime.rawTime
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
:
↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
The genuine full energy-order nonlinear raw time field, constructed using maximal regularity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionEnergyTime.sourceTime
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
:
↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
The actual full energy-order projected nonlinear forcing belongs to Bochner L² time.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionEnergyTime.signedPressureTime
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
:
↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
The actual signed coercive pressure has full energy-order Bochner regularity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionEnergyTime.weightedCorrectionForcing
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(hG : Continuous fun (t : ↑(Set.Icc 0 T)) => (D.metric.coefficient t).operator)
(N : ℕ)
(hN : N + 6 ≤ q + 1)
(R : C(↑(Set.Icc 0 T), ℝ))
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q))))
:
↥(EulerTimeLp.TimeLp T ℝ)
The actual limiting weighted word forcing constructed from the genuine correction time fields.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionEnergyTime.correctionArray
(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)
(e : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(V : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1)))
(τ : ↑(Set.Icc 0 T))
:
The seven literal spatial correction terms evaluated on an actual higher Sobolev representative.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionEnergyTime.weightedCorrectionForcing_ae
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q + 1)
(T : ℝ)
(hT : 0 ≤ T)
(D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 T))
(hG : 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), ℝ))
(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))
:
↑↑(weightedCorrectionForcing period hq T hT D hG N hN R e U) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) =>
EulerWeightedCylinderEnergy.weightedForcingSum (R (Set.projIcc 0 T hT t))
(fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst)
(correctionArray period hq D K6 N hN e (↑↑(EulerSobolevWordValueIdentity.reindexMaximalTime period q T U) t)
(Set.projIcc 0 T hT t))
The constructed actual weighted time forcing is exactly the seven genuine correction terms almost everywhere.