The actual mean velocity and pressure-gradient residual

From a genuine strong mean evolution, construct B=F z_t in Bochner L², its actual time derivative, and the residual f-B_t-MB. Its F-adjoint transform is in the ordinary L² gradient space by the proved strong projected equation.

noncomputable def EulerMeanVariationalInverse.StrongMeanEvolution.velocityField {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) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

The actual physical velocity B=F z_t as a Bochner L² field.

Equations

• s.velocityField = (EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) s.velocityLp

noncomputable def EulerMeanVariationalInverse.StrongMeanEvolution.physicalPath {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) : ℝ → ↥EulerMeanSolenoidal.L2

The actual continuous physical-velocity representative.

Equations

• s.physicalPath t = (EulerVolterraConvolution.extendPath T hT F t) ↑(s.velocity t)

noncomputable def EulerMeanVariationalInverse.StrongMeanEvolution.velocityDerivative {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) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

The product-rule candidate for B_t, constructed in actual Bochner L².

Equations

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

theorem EulerMeanVariationalInverse.StrongMeanEvolution.physical_h1 {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) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t) : AbsolutelyContinuousOnInterval s.physicalPath 0 T ∧ ↑↑s.velocityField =ᵐ[EulerTimeLp.timeMeasure T] s.physicalPath ∧ ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt s.physicalPath (↑↑s.velocityDerivative t) t

This field really is B_t, and B has an actual absolutely continuous representative.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.inversePhysicalPath_solenoidal {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) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) ((F t) x) = x) (t : ℝ) : (EulerVolterraConvolution.extendPath T hT FInv t) (s.physicalPath t) ∈ EulerMeanSolenoidal.solenoidalSpace

In label coordinates the actual physical velocity is solenoidal at every time.

noncomputable def EulerMeanVariationalInverse.StrongMeanEvolution.pressureResidual {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) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

The pressure residual in the strong equation, before using F_t=MF.

Equations

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

theorem EulerMeanVariationalInverse.StrongMeanEvolution.pressureResidual_ae {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) : ↑↑s.pressureResidual =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => ↑↑f t - (EulerVolterraConvolution.extendPath T hT F t) ↑(↑↑s.acceleration t) - 2 • (EulerVolterraConvolution.extendPath T hT F₁ t) ↑(s.velocity t)

The residual has its literal pointwise strong-equation representative.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.pressureResidual_gradient_ae {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) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, (ContinuousLinearMap.adjoint (EulerVolterraConvolution.extendPath T hT F t)) (↑↑s.pressureResidual t) ∈ EulerMeanSolenoidal.gradientSpace

The actual pressure residual has an ordinary weak L² gradient after F-adjoint transformation. This follows from the proved projected equation.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.movingVelocityField_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) (M : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hM : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F₁ t) x = (M t) ((F t) x)) : (EulerTimeLp.timeMultiplier T hT M) s.velocityField = (EulerTimeLp.timeMultiplier T hT (solenoidalFrame T F₁)) s.velocityLp

The prescribed coefficient identity F_t=MF holds for the actual velocity field.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocity_evolution {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) (M : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hM : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F₁ t) x = (M t) ((F t) x)) : s.velocityDerivative + (EulerTimeLp.timeMultiplier T hT M) s.velocityField + s.pressureResidual = f

The reconstructed fields satisfy the actual evolution B_t+MB+dq=f in L².

theorem EulerMeanVariationalInverse.StrongMeanEvolution.physicalPath_initial {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) (hF₀ : F ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) : s.physicalPath 0 = L • A ↑(s.label 0)

The initial physical velocity is exactly the source's localized boundary value.