Admissible raw mean forcing and its actual solved continuous paths

Admissibility consists of literal smooth spatial L² slices and continuity of their L² spatial jets. All translation regularity below is derived. The solution paths are obtained by the concrete source inverse in MeanPacketData.

Actual spatial derivatives of the forcing supply the time-space translation hypotheses.

Smooth parameter dependence in actual L² from square-integrable fiberwise jets.

structure EulerLpSmoothFamily.SmoothFamily {X : Type u} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (P : Type v) (V : Type w) [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] : Type (max (max u v) w)

Actual parameter jets on almost every fiber, with one L² majorant per derivative order.

• field : P → X → V

  Underlying field of SmoothFamily, of type P → X → V.

• smooth : ∀ᵐ (x : X) ∂μ, ContDiff ℝ ↑⊤ fun (a : P) => self.field a x
• jet (n : ℕ) : P → ↥(MeasureTheory.Lp (P [×n]→L[ℝ] V) 2 μ)

  Jet of SmoothFamily, of type (n : ℕ) → P → Lp (P [×n]→L[ℝ] V) 2 μ.

• jet_ae (n : ℕ) (a : P) : ↑↑(self.jet n a) =ᵐ[μ] fun (x : X) => iteratedFDeriv ℝ n (fun (b : P) => self.field b x) a
• bound : ℕ → ↥(MeasureTheory.Lp ℝ 2 μ)

  Bound of SmoothFamily, of type ℕ → Lp ℝ 2 μ.

• bounded (n : ℕ) : ∀ᵐ (x : X) ∂μ, ∀ (a : P), ‖iteratedFDeriv ℝ n (fun (b : P) => self.field b x) a‖ ≤ ↑↑(self.bound n) x

noncomputable def EulerLpSmoothFamily.SmoothFamily.value {X : Type u} [MeasurableSpace X] {P : Type v} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure X} (A : SmoothFamily μ P V) (a : P) : ↥(MeasureTheory.Lp V 2 μ)

Value, given by (continuousMultilinearCurryFin0 ℝ P V).toContinuousLinearEquiv.toContinuousLinearMap.compLpL 2 μ (A.jet 0 a).

Equations

• A.value a = (ContinuousLinearMap.compLpL 2 μ ↑↑(continuousMultilinearCurryFin0 ℝ P V)) (A.jet 0 a)

theorem EulerLpSmoothFamily.SmoothFamily.value_ae {X : Type u} [MeasurableSpace X] {P : Type v} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure X} (A : SmoothFamily μ P V) (a : P) : ↑↑(A.value a) =ᵐ[μ] A.field a

noncomputable def EulerLpSmoothFamily.SmoothFamily.derivative {X : Type u} [MeasurableSpace X] {P : Type v} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure X} (A : SmoothFamily μ P V) : SmoothFamily μ P (P →L[ℝ] V)

Derivative, bundling field, smooth, jet, jet_ae and the required compatibility proofs.

Equations

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

theorem EulerLpSmoothFamily.SmoothFamily.bound_nonneg {X : Type u} [MeasurableSpace X] {P : Type v} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure X} (A : SmoothFamily μ P V) (n : ℕ) : ∀ᵐ (x : X) ∂μ, 0 ≤ ↑↑(A.bound n) x

theorem EulerLpSmoothFamily.SmoothFamily.hasFDerivAt_value {X : Type u} [MeasurableSpace X] {P : Type v} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure X} (A : SmoothFamily μ P V) (a : P) : HasFDerivAt A.value (EulerLpDerivative.derivativeMap μ (A.derivative.value a)) a

theorem EulerLpSmoothFamily.SmoothFamily.fderiv_value {X : Type u} [MeasurableSpace X] {P : Type v} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure X} (A : SmoothFamily μ P V) : fderiv ℝ A.value = fun (a : P) => (EulerLpDerivative.derivativeBundling μ) (A.derivative.value a)

All-order L² parameter regularity with the original square-integrable derivative bounds.

theorem EulerLpSmoothFamily.SmoothFamily.contDiff_value {X : Type u} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothFamily μ P V) : ContDiff ℝ (↑⊤) A.value

Genuine smoothness in the full L² norm, not merely pointwise in the measured variable.

theorem EulerLpSmoothFamily.SmoothFamily.norm_value_le {X : Type u} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothFamily μ P V) (a : P) : ‖A.value a‖ ≤ ‖A.bound 0‖

theorem EulerLpSmoothFamily.SmoothFamily.norm_iteratedFDeriv_value_le {X : Type u} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {P : Type} [NormedAddCommGroup P] [NormedSpace ℝ P] {V : Type w} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothFamily μ P V) (n : ℕ) (a : P) : ‖iteratedFDeriv ℝ n A.value a‖ ≤ ‖A.bound n‖

Each true L² derivative inherits its original fiberwise L² majorant with constant one.

theorem EulerMeanForcing.orbitJet_memLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (A : ℝ → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (A t).jetLp n) 2 (EulerTimeLp.timeMeasure T)) (n : ℕ) (a : EulerSmoothLimit.Space) : MeasureTheory.MemLp (fun (t : ℝ) => iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerLpTranslation.translation b) (A t).toLp) a) 2 (EulerTimeLp.timeMeasure T)

noncomputable def EulerMeanForcing.forcingFamily {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (A : ℝ → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (A t).jetLp n) 2 (EulerTimeLp.timeMeasure T)) : EulerLpSmoothFamily.SmoothFamily (EulerTimeLp.timeMeasure T) EulerSmoothLimit.Space ↥(EulerLpTranslation.L2Space V)

Forcing family, bundling field, smooth, jet, jet_ae and the required compatibility proofs.

Equations

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

theorem EulerMeanForcing.forcingFamily_value_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (A : ℝ → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (A t).jetLp n) 2 (EulerTimeLp.timeMeasure T)) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpTranslation.L2Space V))) (hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (A t).toLp) (a : EulerSmoothLimit.Space) : (forcingFamily T A hA).value a = (EulerTimeLpBoundedMap.timeLiftIsometry T (EulerLpTranslation.translation a)) f

theorem EulerMeanForcing.forcing_translation_contDiff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (A : ℝ → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (A t).jetLp n) 2 (EulerTimeLp.timeMeasure T)) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpTranslation.L2Space V))) (hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (A t).toLp) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerTimeLpBoundedMap.timeLiftIsometry T (EulerLpTranslation.translation a)) f

Smooth forcing slices with actual square-integrable spatial jets have a smooth Bochner translation orbit.

theorem EulerMeanForcing.forcing_translation_jet_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (A : ℝ → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), MeasureTheory.MemLp (fun (t : ℝ) => (A t).jetLp n) 2 (EulerTimeLp.timeMeasure T)) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpTranslation.L2Space V))) (hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (A t).toLp) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (b : EulerSmoothLimit.Space) => (EulerTimeLpBoundedMap.timeLiftIsometry T (EulerLpTranslation.translation b)) f) a‖ ≤ ‖MeasureTheory.MemLp.toLp (fun (t : ℝ) => (A t).jetLp n) ⋯‖

The true time-space derivative norm is bounded by the original ordinary spatial jet norm, without extra factors.

Continuous ordinary forcing jets supply the Bochner hypotheses

On the compact time interval, continuous actual spatial L² jets are automatically square integrable. The continuous and Bochner orbit theorems therefore use the same concrete forcing data.

theorem EulerContinuousForcing.spatialJets_memLp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A : ℝ → EulerLpTranslation.SmoothL2Field V) (hA : ∀ (n : ℕ), Continuous fun (t : ↑(Set.Icc 0 T)) => (A ↑t).jetLp n) (n : ℕ) : MeasureTheory.MemLp (fun (t : ℝ) => (A t).jetLp n) 2 (EulerTimeLp.timeMeasure T)

theorem EulerContinuousForcing.forcing_representation {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (T : ℝ) (hT : 0 ≤ T) (A : ℝ → EulerLpTranslation.SmoothL2Field V) (fC : C(↑(Set.Icc 0 T), ↥(EulerLpTranslation.L2Space V))) (hC : ∀ (t : ↑(Set.Icc 0 T)), fC t = (A ↑t).toLp) (f : ↥(EulerTimeLp.TimeLp T ↥(EulerLpTranslation.L2Space V))) (hf : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT fC) : ↑↑f =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => (A t).toLp

structure EulerMeanPacketProvider.Forcing (D : Data) (raw : EulerPacketProfileRecursion.VectorField) : Type

Literal raw-field regularity, with no hypothesis on a solved field.

• slices : ℝ → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Slices of Forcing, of type ℝ → EulerLpTranslation.SmoothL2Field Space.

• jets_continuous (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 D.T)) => (self.slices ↑t).jetLp n
• path : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2)

  Time-dependent path of Forcing, of type C(Icc (0 : ℝ) D.T,L2).

• path_eq (t : ↑(Set.Icc 0 D.T)) : self.path t = (self.slices ↑t).toLp
• raw_eq (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : raw (↑t, x, θ) = (self.slices ↑t).field x

theorem EulerMeanPacketProvider.Data.opF_orbit (D : Data) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath D.T a D.opF

theorem EulerMeanPacketProvider.Data.opF₁_orbit (D : Data) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => EulerMeanOperatorTranslation.translatePath D.T a D.opF₁

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

noncomputable def EulerMeanPacketProvider.Forcing.lp {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ↥(EulerTimeLp.TimeLp D.T ↥EulerMeanSolenoidal.L2)

The genuine Bochner L² class of the prescribed forcing.

Equations

• G.lp = EulerTimeLp.pathLp D.T ⋯ G.path

theorem EulerMeanPacketProvider.Forcing.lp_rep {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ↑↑G.lp =ᵐ[EulerTimeLp.timeMeasure D.T] EulerVolterraConvolution.extendPath D.T ⋯ G.path

theorem EulerMeanPacketProvider.Forcing.lp_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeTranslation D.T a) G.lp

theorem EulerMeanPacketProvider.Forcing.path_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T a) G.path

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Forcing.solution {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : EulerMeanVariationalInverse.StrongMeanEvolution D.T ⋯ D.opInv D.opF D.opF₁ (EulerMeanBoundary.boundaryOperator (EulerMeanBoundary.scaledCutoff D.ℓ ⋯)) D.L (↑(D.solver G.lp)) G.lp

Solution: an abbreviation for D.evolution G.lp.

Equations

• G.solution = D.evolution G.lp

theorem EulerMeanPacketProvider.Forcing.coordinate_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation D.T a) G.solution.velocityLp

Spatial smoothness of the actually solved coordinate velocity.

theorem EulerMeanPacketProvider.Forcing.acceleration_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeTranslation.timeSolenoidalTranslation D.T a) G.solution.acceleration

theorem EulerMeanPacketProvider.Forcing.coordinatePath_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation D.T a) G.solution.coordinateVelocityPath

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Forcing.velocityPath {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2)

Velocity path: an abbreviation for G.solution.continuousVelocity.

Equations

• G.velocityPath = G.solution.continuousVelocity

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Forcing.accelerationPath {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.solenoidalSpace)

Acceleration path: an abbreviation for G.solution.classicalAcceleration D.frameLower D.frameLower_pos D.frame_lower G.path.

Equations

• G.accelerationPath = G.solution.classicalAcceleration D.frameLower ⋯ ⋯ G.path

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Forcing.derivativePath {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2)

Derivative path: an abbreviation for G.solution.classicalPhysicalDerivative D.frameLower D.frameLower_pos D.frame_lower G.path.

Equations

• G.derivativePath = G.solution.classicalPhysicalDerivative D.frameLower ⋯ ⋯ G.path

@[reducible, inline]

noncomputable abbrev EulerMeanPacketProvider.Forcing.pressureForcePath {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : C(↑(Set.Icc 0 D.T), ↥EulerMeanSolenoidal.L2)

Pressure force path: an abbreviation for G.solution.pressurePath D.frameLower D.frameLower_pos D.frame_lower G.path.

Equations

• G.pressureForcePath = G.solution.pressurePath D.frameLower ⋯ ⋯ G.path

theorem EulerMeanPacketProvider.Forcing.velocityPath_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T a) G.velocityPath

theorem EulerMeanPacketProvider.Forcing.accelerationPath_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanCoordinatePath.coordinatePathTranslation D.T a) G.accelerationPath

theorem EulerMeanPacketProvider.Forcing.derivativePath_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T a) G.derivativePath

theorem EulerMeanPacketProvider.Forcing.pressureForcePath_orbit {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : ContDiff ℝ ↑⊤ fun (a : EulerSmoothLimit.Space) => (EulerMeanTimeContinuousTranslation.pathTranslation D.T a) G.pressureForcePath

theorem EulerMeanPacketProvider.Forcing.velocityPath_time {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (t : ↑(Set.Icc 0 D.T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath D.T ⋯ G.velocityPath) (G.derivativePath t) (Set.Icc 0 D.T) ↑t