The actual source mean inverse on a fixed spatial Hilbert space

The lower boundary bound is discharged by the proved harmonic localization estimate. Coefficients are actual bounded smooth matrix fields. The fixed coordinate solver is identified with the original source mean solver, and its spatial translation regularity follows from the constructed coefficient families.

@[instance_reducible]

noncomputable def EulerMeanSourceFixedInverse.instMeanSourceFixedInverse1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceFixedInverse.instMeanSourceFixedInverse1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceFixedInverse.instMeanSourceFixedInverse2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanSourceFixedInverse.instMeanSourceFixedInverse2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceFixedInverse.instMeanSourceFixedInverse3 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceFixedInverse.instMeanSourceFixedInverse3 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceFixedInverse.instMeanSourceFixedInverse4 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceFixedInverse.instMeanSourceFixedInverse4 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceFixedInverse.instMeanSourceFixedInverse5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceFixedInverse.instMeanSourceFixedInverse5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanSourceFixedInverse.instMeanSourceFixedInverse6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanSourceFixedInverse.instMeanSourceFixedInverse6 T = inferInstance

noncomputable def EulerMeanSourceFixedInverse.sourceFixedForm (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (L : ℝ) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The actual full source form on fixed solenoidal derivative coordinates.

Equations

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

noncomputable def EulerMeanSourceFixedInverse.sourceFixedCoercivity (T : ℝ) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : ℝ

The positive source coercivity constant uses the actual inverse-frame bound.

Equations

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

theorem EulerMeanSourceFixedInverse.sourceFixedCoercivity_pos (T : ℝ) (hT : 0 ≤ T) (F F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : 0 < sourceFixedCoercivity T F F₁ FInv

theorem EulerMeanSourceFixedInverse.sourceFixedForm_coercive (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : sourceFixedCoercivity T F F₁ FInv * ‖v‖ ^ 2 ≤ inner ℝ ((sourceFixedForm T hT ℓ hℓ F F₁ H M0 L) v) v

The source's spatial and time assumptions imply fixed-space coercivity.

noncomputable def EulerMeanSourceFixedInverse.sourceCoordinateSolver (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

The fixed coordinate source solver is constructed from the proved coercive form.

Equations

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

theorem EulerMeanSourceFixedInverse.sourceCoordinateSolver_eq_mean (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), ((EulerMeanCoefficients.operatorPath T F.field) t) ((FInv t) x) = x) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (sourceCoordinateSolver T hT ℓ hℓ F F₁ H M0 FInv Be Bc L r hBe hBc hL hr hrquarter hext hcore hInv hF K hK hF0 hH hsmall) f = (EulerMeanVariationalInverse.meanBackward T hT FInv (EulerMeanCoefficients.operatorPath T F.field) (EulerMeanCoefficients.operatorPath T F₁.field) hInv) ((EulerMeanSourceInverse.sourceMeanSolver T hT ℓ hℓ ⇑M0.field ⋯ ‖M0.field‖₊ ⋯ Be Bc L r hBe hBc hL hr hrquarter hext hcore FInv (EulerMeanCoefficients.operatorPath T H.field) K hK hF0 ⋯ hsmall) f)

The new fixed representation is exactly the original actual source solver in coordinates.

theorem EulerMeanSourceFixedInverse.sourceCoordinateSolver_translation_contDiff (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (F F₁ H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) (FInv : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (Be Bc L r : ℝ) (hBe : 0 ≤ Be) (hBc : 0 ≤ Bc) (hL : EulerMeanHarmonic.boundaryLocalizationC1 * Bc ≤ L) (hr : 0 ≤ r) (hrquarter : r ≤ 1 / 4) (hext : ∀ (x : EulerSmoothLimit.Space), r ≤ ‖ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -Be * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M0.field x) v) v) (hInv : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (FInv t) (((EulerMeanCoefficients.operatorPath T F.field) t) x) = x) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (EulerMeanCoefficients.operatorPath T F.field)) ((EulerMeanCoefficients.operatorPath T F₁.field) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), inner ℝ (((H.field t) x) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (hf : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation T a) f) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((sourceCoordinateSolver T hT ℓ hℓ F F₁ H M0 FInv Be Bc L r hBe hBc hL hr hrquarter hext hcore hInv hF K hK hF0 hH hsmall) f)

Actual smooth coefficients and a smooth forcing orbit imply a smooth source-solution orbit; no inverse regularity or coercivity premise remains to be supplied.