The actual continuous mean pressure residual #
The residual is constructed from the genuine continuous Gram acceleration. Its F-adjoint lies in the ordinary closed gradient space at every time. The true physical equation and fixed-Sobolev estimates hold in the same continuous path space, including the interval endpoints.
Genuine mean momentum regularity from the variational solve #
Zero-initial-trace solenoidal test primitives are mapped by F into the actual
mean test space. The two original boundary terms then vanish, and the weak
identity constructs an AC representative of Pσ F* η_t. This is a regularity
conclusion, not an assumed momentum equation or an assumed second derivative.
theorem
EulerMeanVariationalInverse.solenoidalFrame_adjoint
(T : ℝ)
(F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(t : ↑(Set.Icc 0 T))
:
The frame adjoint is the actual ordinary solenoidal projection of F*.
theorem
EulerMeanVariationalInverse.meanMomentum_ae
(T : ℝ)
(hT : 0 ≤ T)
(F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
:
(fun (t : ℝ) =>
↑(↑↑(EulerTransverseMomentumRegularity.momentum T hT (solenoidalFrame T F) u) t)) =ᵐ[EulerTimeLp.timeMeasure T]
fun (t : ℝ) =>
EulerMeanSolenoidal.solenoidalProjection
((ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT F t)) (↑↑u t))
Thus the momentum's actual representative is Pσ F* u, with ordinary
spatial L² projection and no abstract replacement of the solenoidal space.
theorem
EulerMeanVariationalInverse.meanMomentum_weak
(T : ℝ)
(hT : 0 ≤ T)
(FInv F F' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F' t) (Set.Icc 0 T) ↑t)
(hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) ((F t) x) = x)
(H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)
(L : ℝ)
(u : ↥(meanDerivatives T hT FInv))
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(hu :
∀ (w : ↥(meanDerivatives T hT FInv)),
inner ℝ ↑u ↑w - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) w) + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) w) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) w) = -inner ℝ f ((meanPrimitive T hT FInv) w))
(v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace))
(hv : (EulerTerminalTimePrimitive.initialTrace T hT) v = 0)
:
inner ℝ (EulerTransverseMomentumRegularity.momentum T hT (solenoidalFrame T F) ↑u) v = -inner ℝ
(EulerTransverseMomentumRegularity.momentumForcing T hT (solenoidalFrame T F) (solenoidalFrame T F') H (↑u) f)
((EulerTerminalTimePrimitive.primitiveTimeLp T hT) v)
The exact mean variational identity determines the weak derivative of its actual projected momentum after the trace-zero test restriction.
theorem
EulerMeanVariationalInverse.meanMomentum_ac
(T : ℝ)
(hT : 0 ≤ T)
(FInv F F' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(hTpos : 0 < T)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F' t) (Set.Icc 0 T) ↑t)
(hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) ((F t) x) = x)
(H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)
(L : ℝ)
(u : ↥(meanDerivatives T hT FInv))
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
(hu :
∀ (w : ↥(meanDerivatives T hT FInv)),
inner ℝ ↑u ↑w - inner ℝ ((EulerTimeLp.timeMultiplier T hT H) ((meanPrimitive T hT FInv) u)) ((meanPrimitive T hT FInv) w) + inner ℝ (M0 ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) w) + L * inner ℝ (A ((meanTrace T hT FInv) u)) ((meanTrace T hT FInv) w) = -inner ℝ f ((meanPrimitive T hT FInv) w))
:
∃ (p : ℝ → ↥EulerMeanSolenoidal.solenoidalSpace),
AbsolutelyContinuousOnInterval p 0 T ∧ ↑↑(EulerTransverseMomentumRegularity.momentum T hT (solenoidalFrame T F) ↑u) =ᵐ[EulerTimeLp.timeMeasure T] p ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt p
(↑↑(EulerTransverseMomentumRegularity.momentumForcing T hT (solenoidalFrame T F) (solenoidalFrame T F') H (↑u)
f)
t)
t
An actual weak mean solution has an AC momentum representative with the explicit Bochner L² derivative forced by the variational identity.
theorem
EulerMeanVariationalInverse.meanSolver_momentum_ac
(T : ℝ)
(hT : 0 ≤ T)
(FInv F F' : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(hTpos : 0 < T)
(hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F' t) (Set.Icc 0 T) ↑t)
(hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) ((F t) x) = x)
(H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)
(L K B : ℝ)
(hK : 0 ≤ K)
(hB : 0 ≤ B)
(hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2)
(hH : ∀ (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.L2), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2)
(hboundary : ∀ z ∈ EulerMeanSolenoidal.solenoidalSpace, -B * ‖z‖ ^ 2 ≤ inner ℝ (M0 z) z + L * inner ℝ (A z) z)
(hsmall : K * (T ^ 2 / 2) + B * T ≤ 1 / 2)
(f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2))
:
have u := ↑((meanSolver T hT FInv H M0 A L K B hK hB hF0 hH hboundary hsmall) f);
∃ (p : ℝ → ↥EulerMeanSolenoidal.solenoidalSpace),
AbsolutelyContinuousOnInterval p 0 T ∧ ↑↑(EulerTransverseMomentumRegularity.momentum T hT (solenoidalFrame T F) u) =ᵐ[EulerTimeLp.timeMeasure T] p ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt p
(↑↑(EulerTransverseMomentumRegularity.momentumForcing T hT (solenoidalFrame T F) (solenoidalFrame T F') H u f)
t)
t
In particular the already constructed mean variational inverse has genuine projected momentum regularity. The coefficient/boundary lower bounds are used only by that solve; no regularity of the answer is assumed.
noncomputable def
EulerMeanVariationalInverse.StrongMeanEvolution.pressurePath
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
:
The physical pressure force in the actual continuous strong equation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.pressurePath_gradient
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(t : ↑(Set.Icc 0 T))
:
(ContinuousLinearMap.adjoint (F t)) ((s.pressurePath c hc hLower fC) t) ∈ EulerMeanSolenoidal.gradientSpace
The projected equation forces the actual pullback residual to be a gradient at every time, not just almost everywhere in time.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.pressurePath_equation
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hTpos : 0 < T)
(hFTime : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t)
(M : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2))
(hMF : ∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.L2), (F₁ t) v = (M t) ((F t) v))
(t : ↑(Set.Icc 0 T))
:
(s.classicalPhysicalDerivative c hc hLower fC) t + (M t) (s.continuousVelocity t) + (s.pressurePath c hc hLower fC) t = fC t
The physical pressure force is exactly f-B_t-MB for the given actual coefficient relation F_t=MF.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.pressurePath_orbit_eq
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
:
(fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)) = ((fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC) - fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T a)
((EulerContinuousTimeIntegral.multiplier (solenoidalFrame T F)) (s.classicalAcceleration c hc hLower fC))) - fun (a : EulerSmoothLimit.Space) =>
2 • (EulerMeanTimeContinuousTranslation.pathTranslation T a)
((EulerContinuousTimeIntegral.multiplier (solenoidalFrame T F₁)) s.coordinateVelocityPath)
The actual spatial orbit of the pressure force has the literal residual formula.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.pressurePath_translation_contDiff
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
(hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F)
(hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁)
(hv :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T a) s.coordinateVelocityPath)
(ha :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T a) (s.classicalAcceleration c hc hLower fC))
(hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC)
:
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T a) (s.pressurePath c hc hLower fC)
Known actual field and coefficient orbits imply pressure-force regularity.
theorem
EulerMeanVariationalInverse.StrongMeanEvolution.pressurePath_translation_block_gevrey
{T : ℝ}
{hT : 0 ≤ T}
{FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)}
{A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2}
{L : ℝ}
{u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)}
(s : StrongMeanEvolution T hT FInv F F₁ A L u f)
(c : ℝ)
(hc : 0 < c)
(hLower :
∀ (t : ↑(Set.Icc 0 T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace), c * ‖v‖ ^ 2 ≤ ‖((solenoidalFrame T F) t) v‖ ^ 2)
(fC : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2))
{ι : Type u_1}
[Fintype ι]
(directions : ι → EulerSmoothLimit.Space)
(hd : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(hF : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F)
(hF₁ : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T a F₁)
(hv :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T a) s.coordinateVelocityPath)
(ha :
ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T a) (s.classicalAcceleration c hc hLower fC))
(hfC : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T a) fC)
(Rc R CF CF₁ Cf Cv Ca : ℝ)
(hRc : 0 ≤ Rc)
(hRcR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R)
(hCF : 0 ≤ CF)
(hCF₁ : 0 ≤ CF₁)
(hCv : 0 ≤ Cv)
(hCa : 0 ≤ Ca)
(d : ℕ)
(hFb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F) a‖ ≤ CF * EulerGevrey.majorant Rc 0 n)
(hF₁b :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath T b F₁) a‖ ≤ CF₁ * EulerGevrey.majorant Rc 0 n)
(hfb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
EulerParameterWordGevrey.block directions q
(fun (b : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation T b) fC) n a ≤ Cf * EulerGevrey.majorant R d n)
(hvb :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
EulerParameterWordGevrey.block directions q
(fun (b : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T b) s.coordinateVelocityPath)
n a ≤ Cv * EulerGevrey.majorant R d n)
(hab :
∀ (n : ℕ) (a : EulerSmoothLimit.Space),
EulerParameterWordGevrey.block directions q
(fun (b : EulerSmoothLimit.Space) =>
(EulerMeanCoordinatePath.coordinatePathTranslation T b) (s.classicalAcceleration c hc hLower fC))
n a ≤ Ca * EulerGevrey.majorant R d n)
(n : ℕ)
(a : EulerSmoothLimit.Space)
:
EulerParameterWordGevrey.block directions q
(fun (b : EulerSmoothLimit.Space) =>
(EulerMeanTimeContinuousTranslation.pathTranslation T b) (s.pressurePath c hc hLower fC))
n a ≤ (Cf + 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF * Ca + 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc CF₁ * Cv) * EulerGevrey.majorant R d n
The actual physical pressure gradient costs no further factorial shift.