Concrete source data for the mean packet provider

This record contains only the given matrix coefficients and the manuscript's pointwise inequalities and time identities. Its solver and strong evolution are the previously constructed actual variational inverse, not input fields.

The actual strong mean inverse under the manuscript's spatial hypotheses.

Strong regularity of the genuinely constructed mean inverse

The result applies the strong-coordinate theorem to the actual coercive solve. The input boundary inequality still has to be supplied by the concrete cutoff operator and harmonic localization. No solution, momentum equation, acceleration, or initial velocity condition is included in the hypotheses.

theorem EulerMeanVariationalInverse.meanSolver_strong (T : ℝ) (hT : 0 ≤ T) (FInv F F₁ 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) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑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) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) (hF₁₀ : F₁ ⟨0, ⋯⟩ = M0) (hODE : ∀ (t : ↑(Set.Icc 0 T)), F₂ t = -H t ∘SL F t) (hAσ : ∀ z ∈ EulerMeanSolenoidal.solenoidalSpace, A z ∈ EulerMeanSolenoidal.solenoidalSpace) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : Nonempty (StrongMeanEvolution T hT FInv F F₁ A L (↑((meanSolver T hT FInv H M0 A L K B hK hB hFInv₀ hH hboundary hsmall) f)) f)

The actual bounded mean solution operator produces a strong mean evolution with the literal projected equation and original initial velocity condition.

theorem EulerMeanSourceInverse.sourceMeanSolver_strong (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (M : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) (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 ℝ ((M x) v) v) (hcore : ∀ (x : EulerSmoothLimit.Space), ‖ℓ • x‖ < r → ∀ (v : EulerSmoothLimit.Space), -Bc * ‖v‖ ^ 2 ≤ inner ℝ ((M x) v) v) (FInv F F₁ F₂ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (K : ℝ) (hK : 0 ≤ K) (hF0 : FInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2) (hH : ∀ (t : ↑(Set.Icc 0 T)) (z : ↥EulerMeanSolenoidal.L2), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2) (hsmall : K * (T ^ 2 / 2) + Be * T + EulerMeanHarmonic.boundaryLocalizationC2 * Bc * r ^ 3 * T ≤ 1 / 2) (hF : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT F) (F₁ t) (Set.Icc 0 T) ↑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) (hRight : ∀ (t : ↑(Set.Icc 0 T)) (x : ↥EulerMeanSolenoidal.L2), (F t) ((FInv t) x) = x) (hF₁₀ : F₁ ⟨0, ⋯⟩ = EulerLiftedPressure.coefficientOperator M hM C hC) (hODE : ∀ (t : ↑(Set.Icc 0 T)), F₂ t = -H t ∘SL F t) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : Nonempty (EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv F F₁ (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L (↑((sourceMeanSolver T hT ℓ hℓ M hM C hC Be Bc L r hBe hBc hL hr hrquarter hext hcore FInv H K hK hF0 hH hsmall) f)) f)

The constructed source mean inverse has H² solenoidal coordinates and the original compact-support-producing initial velocity condition.

theorem EulerMeanSourceInverse.sourceStrong_initial_ae_support (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (L : ℝ) (u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (S : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv F F₁ (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L u f) : ∀ᵐ (x : EulerSmoothLimit.Space), 2 < ‖ℓ • x‖ → ↑↑↑(S.velocity 0) x = 0

theorem EulerMeanSourceInverse.sourceStrong_initial_compact (T : ℝ) (hT : 0 ≤ T) (ℓ : ℝ) (hℓ : 0 < ℓ) (FInv F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (L : ℝ) (u f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (S : EulerMeanVariationalInverse.StrongMeanEvolution T hT FInv F F₁ (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff ℓ hℓ)) L u f) (b : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hb : Continuous b) (hrep : b =ᵐ[MeasureTheory.volume] ↑↑↑(S.velocity 0)) : HasCompactSupport b

A continuous representative of the actual initial mean velocity is compactly supported.

structure EulerMeanPacketProvider.Data : Type

Literal coefficient data and source smallness hypotheses.

• T : ℝ

  Time horizon of Data, of type ℝ.

• T_pos : 0 < self.T
• ℓ : ℝ

  ℓ of Data, of type ℝ.

• ℓ_pos : 0 < self.ℓ
• ℓ_le_one : self.ℓ ≤ 1
• F : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 self.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  F of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

• F₁ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 self.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  F₁ of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

• F₂ : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 self.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  F₂ of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

• M : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 self.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  M of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

• H : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 self.T)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  H of Data, of type SmoothCoefficientPath (Icc (0 : ℝ) T) (Space →L[ℝ] Space).

• FInv : C(↑(Set.Icc 0 self.T), EulerMeanCoefficients.Field)

  F inv of Data, of type C(Icc (0 : ℝ) T,Field).

• M0 : EulerMeanCoefficients.BoundedSmoothField (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

  M0 of Data, of type BoundedSmoothField (Space →L[ℝ] Space).

• Be : ℝ

  Be of Data, of type ℝ.

• Bc : ℝ

  Bc of Data, of type ℝ.

• L : ℝ

  L of Data, of type ℝ.

• r : ℝ

  R of Data, of type ℝ.

• K : ℝ

  K of Data, of type ℝ.

• Be_nonneg : 0 ≤ self.Be
• Bc_nonneg : 0 ≤ self.Bc
• L_lower : EulerMeanHarmonic.boundaryLocalizationC1 * self.Bc ≤ self.L
• r_nonneg : 0 ≤ self.r
• r_le_quarter : self.r ≤ 1 / 4
• K_nonneg : 0 ≤ self.K
• exterior_lower (x : EulerSmoothLimit.Space) : self.r ≤ ‖self.ℓ • x‖ → ∀ (v : EulerSmoothLimit.Space), -self.Be * ‖v‖ ^ 2 ≤ inner ℝ ((self.M0.field x) v) v
• core_lower (x : EulerSmoothLimit.Space) : ‖self.ℓ • x‖ < self.r → ∀ (v : EulerSmoothLimit.Space), -self.Bc * ‖v‖ ^ 2 ≤ inner ℝ ((self.M0.field x) v) v
• inverse_left (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : ((self.FInv t) x) (((self.F.field t) x) v) = v
• inverse_right (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : ((self.F.field t) x) (((self.FInv t) x) v) = v
• inverse_initial (x v : EulerSmoothLimit.Space) : ((self.FInv ⟨0, ⋯⟩) x) v = v
• derivative_initial (x : EulerSmoothLimit.Space) : (self.F₁.field ⟨0, ⋯⟩) x = self.M0.field x
• frame_time (t : ℝ) : t ∈ Set.Icc 0 self.T → ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath self.T ⋯ self.F.field s) x) ((EulerVolterraConvolution.extendPath self.T ⋯ self.F₁.field t) x) (Set.Icc 0 self.T) t
• derivative_time (t : ℝ) : t ∈ Set.Icc 0 self.T → ∀ (x : EulerSmoothLimit.Space), HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath self.T ⋯ self.F₁.field s) x) ((EulerVolterraConvolution.extendPath self.T ⋯ self.F₂.field t) x) (Set.Icc 0 self.T) t
• second_equation (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : ((self.F₂.field t) x) v = -((self.H.field t) x) (((self.F.field t) x) v)
• strain_equation (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : ((self.F₁.field t) x) v = ((self.M.field t) x) (((self.F.field t) x) v)
• curvature_upper (t : ↑(Set.Icc 0 self.T)) (x v : EulerSmoothLimit.Space) : inner ℝ (((self.H.field t) x) v) v ≤ self.K * ‖v‖ ^ 2
• small : self.K * (self.T ^ 2 / 2) + self.Be * self.T + EulerMeanHarmonic.boundaryLocalizationC2 * self.Bc * self.r ^ 3 * self.T ≤ 1 / 2

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Data.opF (D : Data) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Op F: an abbreviation for operatorPath D.T D.F.field.

Equations

• D.opF = EulerMeanCoefficients.operatorPath D.T D.F.field

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Data.opF₁ (D : Data) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Op F₁: an abbreviation for operatorPath D.T D.F₁.field.

Equations

• D.opF₁ = EulerMeanCoefficients.operatorPath D.T D.F₁.field

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Data.opF₂ (D : Data) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Op F₂: an abbreviation for operatorPath D.T D.F₂.field.

Equations

• D.opF₂ = EulerMeanCoefficients.operatorPath D.T D.F₂.field

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Data.opM (D : Data) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Op M: an abbreviation for operatorPath D.T D.M.field.

Equations

• D.opM = EulerMeanCoefficients.operatorPath D.T D.M.field

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Data.opH (D : Data) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Op H: an abbreviation for operatorPath D.T D.H.field.

Equations

• D.opH = EulerMeanCoefficients.operatorPath D.T D.H.field

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Data.opInv (D : Data) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Op inv: an abbreviation for operatorPath D.T D.FInv.

Equations

• D.opInv = EulerMeanCoefficients.operatorPath D.T D.FInv

theorem EulerMeanPacketProvider.Data.opInv_left (D : Data) (t : ↑(Set.Icc 0 D.T)) (v : ↥EulerMeanSolenoidal.L2) : (D.opInv t) ((D.opF t) v) = v

theorem EulerMeanPacketProvider.Data.opInv_right (D : Data) (t : ↑(Set.Icc 0 D.T)) (v : ↥EulerMeanSolenoidal.L2) : (D.opF t) ((D.opInv t) v) = v

theorem EulerMeanPacketProvider.Data.opInv_initial (D : Data) : D.opInv ⟨0, ⋯⟩ = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2

theorem EulerMeanPacketProvider.Data.opF_time (D : Data) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ D.opF) (D.opF₁ t) (Set.Icc 0 D.T) ↑t

theorem EulerMeanPacketProvider.Data.opF₁_time (D : Data) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ D.opF₁) (D.opF₂ t) (Set.Icc 0 D.T) ↑t

theorem EulerMeanPacketProvider.Data.opF₁_initial (D : Data) : D.opF₁ ⟨0, ⋯⟩ = EulerLiftedPressure.coefficientOperator ⇑D.M0.field ⋯ ‖D.M0.field‖₊ ⋯

theorem EulerMeanPacketProvider.Data.opF₂_eq (D : Data) (t : ↑(Set.Icc 0 D.T)) : D.opF₂ t = -D.opH t ∘SL D.opF t

theorem EulerMeanPacketProvider.Data.opStrain_eq (D : Data) (t : ↑(Set.Icc 0 D.T)) (v : ↥EulerMeanSolenoidal.L2) : (D.opF₁ t) v = (D.opM t) ((D.opF t) v)

theorem EulerMeanPacketProvider.Data.opCurvature_upper (D : Data) (t : ↑(Set.Icc 0 D.T)) (v : ↥EulerMeanSolenoidal.L2) : inner ℝ ((D.opH t) v) v ≤ D.K * ‖v‖ ^ 2

noncomputable def EulerMeanPacketProvider.Data.solver (D : Data) : ↥(EulerTimeLp.TimeLp D.T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(EulerMeanVariationalInverse.meanDerivatives D.T ⋯ D.opInv)

The actual source weak inverse with the harmonic boundary estimate discharged.

Equations

• D.solver = EulerMeanSourceInverse.sourceMeanSolver D.T ⋯ D.ℓ ⋯ ⇑D.M0.field ⋯ ‖D.M0.field‖₊ ⋯ D.Be D.Bc D.L D.r ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ D.opInv D.opH D.K ⋯ ⋯ ⋯ ⋯

noncomputable def EulerMeanPacketProvider.Data.evolution (D : Data) (f : ↥(EulerTimeLp.TimeLp D.T ↥EulerMeanSolenoidal.L2)) : EulerMeanVariationalInverse.StrongMeanEvolution D.T ⋯ D.opInv D.opF D.opF₁ (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff D.ℓ ⋯)) D.L (↑(D.solver f)) f

The source strong evolution is obtained from the constructed inverse.

Equations

• D.evolution f = Classical.choice ⋯

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Data.frameLower (D : Data) : ℝ

Frame lower: an abbreviation for meanFrameCoercivity D.T D.opInv.

Equations

• D.frameLower = EulerMeanVariationalInverse.meanFrameCoercivity D.T D.opInv

theorem EulerMeanPacketProvider.Data.frameLower_pos (D : Data) : 0 < D.frameLower

theorem EulerMeanPacketProvider.Data.frame_lower (D : Data) (t : ↑(Set.Icc 0 D.T)) (v : ↥EulerMeanSolenoidal.solenoidalSpace) : D.frameLower * ‖v‖ ^ 2 ≤ ‖((EulerMeanVariationalInverse.solenoidalFrame D.T D.opF) t) v‖ ^ 2