Genuine matrix-frame identities induce the operator identities used by the mean inverse.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientFrame1 : NormedAddCommGroup Field

Cache the standard NormedAddCommGroup Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instMeanCoefficientFrame1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.instMeanCoefficientFrame2 : NormedSpace ℝ Field

Cache the standard NormedSpace ℝ Field instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.instMeanCoefficientFrame2 = inferInstance

noncomputable def EulerMeanCoefficients.adjointField (A : Field) : Field

Adjoint field as an element of Field.

Equations

• EulerMeanCoefficients.adjointField A = (ContinuousLinearMap.compLeftContinuousBounded EulerSmoothLimit.Space ↑↑ContinuousLinearMap.adjoint) A

@[simp]

theorem EulerMeanCoefficients.adjointField_apply (A : Field) (x : EulerSmoothLimit.Space) : (adjointField A) x = ContinuousLinearMap.adjoint (A x)

theorem EulerMeanCoefficients.multiplier_adjointField (A : Field) : multiplier (adjointField A) = ContinuousLinearMap.adjoint (multiplier A)

theorem EulerMeanCoefficients.operatorPath_comp (T : ℝ) (A B C : C(↑(Set.Icc 0 T), Field)) (hABC : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), ((C t) x) v = ((A t) x) (((B t) x) v)) (t : ↑(Set.Icc 0 T)) (u : ↥EulerMeanSolenoidal.L2) : ((operatorPath T C) t) u = ((operatorPath T A) t) (((operatorPath T B) t) u)

theorem EulerMeanCoefficients.operatorPath_neg_comp (T : ℝ) (A B C : C(↑(Set.Icc 0 T), Field)) (hABC : ∀ (t : ↑(Set.Icc 0 T)) (x v : EulerSmoothLimit.Space), ((C t) x) v = -((A t) x) (((B t) x) v)) (t : ↑(Set.Icc 0 T)) (u : ↥EulerMeanSolenoidal.L2) : ((operatorPath T C) t) u = -((operatorPath T A) t) (((operatorPath T B) t) u)

theorem EulerMeanCoefficients.operatorPath_identity_at (T : ℝ) (A : C(↑(Set.Icc 0 T), Field)) (t : ↑(Set.Icc 0 T)) (hA : ∀ (x v : EulerSmoothLimit.Space), ((A t) x) v = v) : (operatorPath T A) t = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2

theorem EulerMeanCoefficients.operatorPath_initial_coefficient (T : ℝ) (hT : 0 ≤ T) (A : C(↑(Set.Icc 0 T), Field)) (M : Field) (hAM : ∀ (x : EulerSmoothLimit.Space), (A ⟨0, ⋯⟩) x = M x) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖M x‖ ≤ ↑C) : (operatorPath T A) ⟨0, ⋯⟩ = EulerLiftedPressure.coefficientOperator ⇑M ⋯ C hC

theorem EulerMeanCoefficients.operatorPath_norm_le (T : ℝ) (A : C(↑(Set.Icc 0 T), Field)) : ‖operatorPath T A‖ ≤ ‖A‖

theorem EulerMeanCoefficients.operatorPath_norm_le_of_pointwise (T : ℝ) (A : C(↑(Set.Icc 0 T), Field)) (C : ℝ) (hC : 0 ≤ C) (hA : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖(A t) x‖ ≤ C) : ‖operatorPath T A‖ ≤ C