Genuine parameter regularity of the fixed mean form

Restricting a coefficient to the ordinary solenoidal space is itself a bounded linear map. The actual time multipliers, H¹ transport, trace, and full mean form therefore inherit parameter regularity from the coefficient paths.

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity1 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity2 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity4 : NormedSpace ℝ (↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity5 : NormedAddCommGroup (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity5 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity6 : NormedSpace ℝ (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

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

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity6 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity7 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity8 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, L2 →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity8 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity9 (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity9 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity10 (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T, solenoidalSpace →L[ℝ] L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedCoefficientRegularity.instMeanFixedCoefficientRegularity10 T = inferInstance

noncomputable def EulerMeanFixedCoefficientRegularity.frameRestriction : (↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2

The actual continuous linear restriction of spatial operators to L²σ.

Equations

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

noncomputable def EulerMeanFixedCoefficientRegularity.framePathRestriction (T : ℝ) : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) →L[ℝ] C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.solenoidalSpace →L[ℝ] ↥EulerMeanSolenoidal.L2)

The actual continuous linear restriction of time-dependent spatial operators.

Equations

• EulerMeanFixedCoefficientRegularity.framePathRestriction T = ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) EulerMeanFixedCoefficientRegularity.frameRestriction

@[simp]

theorem EulerMeanFixedCoefficientRegularity.framePathRestriction_apply (T : ℝ) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) : (framePathRestriction T) F = EulerMeanVariationalInverse.solenoidalFrame T F

theorem EulerMeanFixedCoefficientRegularity.framePathRestriction_norm (T : ℝ) : ‖framePathRestriction T‖ ≤ 1

Solenoidal frame restriction is a norm contraction.

theorem EulerMeanFixedCoefficientRegularity.contDiff_solenoidalFrame {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (F : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hF : ContDiff ℝ n F) : ContDiff ℝ n fun (p : P) => EulerMeanVariationalInverse.solenoidalFrame T (F p)

The actual restricted frame has the given parameter regularity.

theorem EulerMeanFixedCoefficientRegularity.contDiff_fixedMeanDerivative {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hF : ContDiff ℝ n F) (hF₁ : ContDiff ℝ n F₁) : ContDiff ℝ n fun (p : P) => EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT (F p) (F₁ p)

The genuine physical derivative map inherits parameter regularity.

theorem EulerMeanFixedCoefficientRegularity.contDiff_fixedMeanPrimitive {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hF : ContDiff ℝ n F) (hF₁ : ContDiff ℝ n F₁) : ContDiff ℝ n fun (p : P) => EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT (F p) (F₁ p)

The genuine displacement primitive map inherits parameter regularity.

theorem EulerMeanFixedCoefficientRegularity.contDiff_fixedMeanTrace {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) {n : WithTop ℕ∞} (hF : ContDiff ℝ n F) (hF₁ : ContDiff ℝ n F₁) : ContDiff ℝ n fun (p : P) => EulerMeanFixedSpaceInverse.fixedMeanTrace T hT (F p) (F₁ p)

The actual initial-trace map inherits parameter regularity.

theorem EulerMeanFixedCoefficientRegularity.contDiff_fixedMeanOperator {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (F F₁ H : P → C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : P → ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) {n : WithTop ℕ∞} (hF : ContDiff ℝ n F) (hF₁ : ContDiff ℝ n F₁) (hH : ContDiff ℝ n H) (hM0 : ContDiff ℝ n M0) (hA : ContDiff ℝ n A) : ContDiff ℝ n fun (p : P) => EulerMeanFixedSpaceInverse.fixedMeanOperator T hT (F p) (F₁ p) (H p) (M0 p) (A p) L

The full mean form, including the nonlocal boundary term, is a genuinely regular family whenever its actual coefficient paths are.