Quantitative time estimates for the genuine mean inverse

The constants depend explicitly and polynomially on the time interval, coefficient bounds, and the inverse-frame bound. The only square roots are the proved finite-time trace/Poincaré factors. These are estimates of the actual Bochner fields and continuous representatives constructed by the inverse.

The actual bounded linear mean velocity inverse

The physical velocity is η_t-F_t F⁻¹η. This formula constructs a bounded linear map on the original derivative variable, and the genuine H² evolution identifies it with F z_t. Composing with the variational solver gives the actual linear velocity inverse with an explicit finite-time bound.

noncomputable def EulerMeanVariationalInverse.meanVelocityMap (T : ℝ) (hT : 0 ≤ T) (FInv F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

The physical velocity formula on actual Bochner derivative fields.

Equations

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

theorem EulerMeanVariationalInverse.meanVelocityMap_ae (T : ℝ) (hT : 0 ≤ T) (FInv F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : ↑↑((meanVelocityMap T hT FInv F₁) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => ↑↑u t - (EulerVolterraConvolution.extendPath T hT F₁ t) ((EulerVolterraConvolution.extendPath T hT FInv t) (EulerTerminalTimePrimitive.realPrimitive T u t))

The bounded linear formula has its literal pointwise representative.

theorem EulerMeanVariationalInverse.meanVelocityMap_apply_norm (T : ℝ) (hT : 0 ≤ T) (FInv F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : ‖(meanVelocityMap T hT FInv F₁) u‖ ≤ (1 + ‖F₁‖ * ‖FInv‖ * √(T ^ 2 / 2)) * ‖u‖

A quantitative bound for the actual linear velocity formula.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.kinetic_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) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑t) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, ↑↑u t = (EulerVolterraConvolution.extendPath T hT F₁ t) ↑(s.label t) + s.physicalPath t

Differentiating the actual displacement reconstruction gives the kinetic identity.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityField_eq_meanVelocityMap {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) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) : s.velocityField = (meanVelocityMap T hT FInv F₁) u

The actual velocity constructed by strong regularity equals the bounded linear formula on the original solved derivative field.

noncomputable def EulerMeanVariationalInverse.meanVelocitySolver (T : ℝ) (hT : 0 ≤ T) (FInv F₁ 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) (hFInv₀ : 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) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

The genuine bounded linear mean velocity inverse on actual forcing classes.

Equations

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

theorem EulerMeanVariationalInverse.meanVelocitySolver_norm (T : ℝ) (hT : 0 ≤ T) (FInv F₁ 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) (hFInv₀ : 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)) : ‖(meanVelocitySolver T hT FInv F₁ H M0 A L K B hK hB hFInv₀ hH hboundary hsmall) f‖ ≤ (1 + ‖F₁‖ * ‖FInv‖ * √(T ^ 2 / 2)) * (2 * T * ‖f‖)

The actual mean velocity inverse has an explicit finite-time bound.

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanStrongEstimates1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanStrongEstimates1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanStrongEstimates2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanStrongEstimates2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanVariationalInverse.instMeanStrongEstimates3 : NormedAddCommGroup (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanVariationalInverse.instMeanStrongEstimates3 = inferInstance

theorem EulerMeanVariationalInverse.solenoidalFrame_norm_le (T : ℝ) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ‖solenoidalFrame T F‖ ≤ ‖F‖

Restricting F to the actual solenoidal subspace does not increase its norm.

theorem EulerMeanVariationalInverse.gram_equation_of_ordinary (F F₁ : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (f : ↥EulerMeanSolenoidal.L2) (a v : ↥EulerMeanSolenoidal.solenoidalSpace) (h : EulerMeanSolenoidal.solenoidalProjection ((ContinuousLinearMap.adjoint F) (F ↑a)) = EulerMeanSolenoidal.solenoidalProjection ((ContinuousLinearMap.adjoint F) (f - 2 • F₁ ↑v))) : (EulerTransverseGramInverse.gram (F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) a = (ContinuousLinearMap.adjoint (F ∘SL EulerMeanSolenoidal.solenoidalSpace.subtypeL)) (f - 2 • F₁ ↑v)

The ordinary projection equation is exactly the Gram equation on L²σ.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityLp_norm_le {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) : ‖s.velocityLp‖ ≤ ‖FInv‖ * ‖s.velocityField‖

Inverse-frame application bounds the actual coordinate velocity by B.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityField_norm {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) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) : ‖s.velocityField‖ ≤ (1 + ‖F₁‖ * ‖FInv‖ * √(T ^ 2 / 2)) * ‖u‖

The actual physical velocity obeys the explicit derivative-variable bound.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityLp_norm_from_input {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) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) ((F t) x) = x) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) : ‖s.velocityLp‖ ≤ ‖FInv‖ * ((1 + ‖F₁‖ * ‖FInv‖ * √(T ^ 2 / 2)) * ‖u‖)

Combining the two actual bounds controls z_t by the original variational variable.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.acceleration_norm {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) : ‖s.acceleration‖ ≤ (‖FInv‖ + 1) ^ 2 * ‖F‖ * (‖f‖ + 2 * ‖F₁‖ * ‖s.velocityLp‖)

The actual strong acceleration pays only the inverse Gram and coefficient norms.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.velocityDerivative_norm {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.velocityDerivative‖ ≤ ‖F₁‖ * ‖s.velocityLp‖ + ‖F‖ * ‖s.acceleration‖

The product-rule derivative B_t has the corresponding actual L² bound.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.pressureResidual_norm {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‖ ≤ ‖f‖ + ‖F‖ * ‖s.acceleration‖ + 2 * ‖F₁‖ * ‖s.velocityLp‖

The actual pressure-gradient residual is controlled without differentiating H.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.initialPhysicalVelocity_norm {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) (hFInv₀ : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hF₀ : F ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) : ‖s.physicalPath 0‖ ≤ |L| * ‖A‖ * √T * ‖u‖

The derived compact-initial-data law has an actual quantitative trace bound.

theorem EulerMeanVariationalInverse.StrongMeanEvolution.physicalPath_norm_uniform {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) (hFInv₀ : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hF₀ : F ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ‖s.physicalPath t‖ ≤ |L| * ‖A‖ * √T * ‖u‖ + √T * ‖s.velocityDerivative‖

The actual continuous velocity is uniformly controlled in time by its initial trace and the proved L² derivative bound.