Continuous matrix fields act as genuine bounded operators on ordinary R³ L².

@[reducible, inline]

abbrev EulerMeanCoefficients.Field : Type

Field: an abbreviation for Space →ᵇ (Space →L[ℝ] Space).

Equations

• EulerMeanCoefficients.Field = BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

noncomputable def EulerMeanCoefficients.multiplier (A : Field) : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Pointwise multiplication by a bounded continuous coefficient field.

Equations

• EulerMeanCoefficients.multiplier A = EulerLiftedPressure.coefficientOperator ⇑A ⋯ ‖A‖₊ ⋯

theorem EulerMeanCoefficients.multiplier_ae (A : Field) (u : ↥EulerMeanSolenoidal.L2) : ↑↑((multiplier A) u) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => (A x) (↑↑u x)

theorem EulerMeanCoefficients.multiplier_norm_le (A : Field) : ‖multiplier A‖ ≤ ‖A‖

theorem EulerMeanCoefficients.multiplier_add (A B : Field) : multiplier (A + B) = multiplier A + multiplier B

theorem EulerMeanCoefficients.multiplier_smul (c : ℝ) (A : Field) : multiplier (c • A) = c • multiplier A

noncomputable def EulerMeanCoefficients.multiplierLinear : Field →ₗ[ℝ] ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Multiplier linear, bundling toFun, map_add, map_smul.

Equations

• EulerMeanCoefficients.multiplierLinear = { toFun := EulerMeanCoefficients.multiplier, map_add' := EulerMeanCoefficients.multiplier_add, map_smul' := EulerMeanCoefficients.multiplier_smul }

noncomputable def EulerMeanCoefficients.multiplierMap : Field →L[ℝ] ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2

Uniform coefficient convergence implies operator-norm convergence by this CLM.

Equations

• EulerMeanCoefficients.multiplierMap = { toLinearMap := EulerMeanCoefficients.multiplierLinear, cont := EulerMeanCoefficients.multiplierMap._proof_3 }

@[simp]

theorem EulerMeanCoefficients.multiplierMap_apply (A : Field) : multiplierMap A = multiplier A

theorem EulerMeanCoefficients.multiplier_one : multiplier 1 = ContinuousLinearMap.id ℝ ↥EulerMeanSolenoidal.L2

theorem EulerMeanCoefficients.multiplier_mul (A B : Field) : multiplier (A * B) = multiplier A ∘SL multiplier B

theorem EulerMeanCoefficients.multiplier_inverse (A B : Field) (hAB : ∀ (x v : EulerSmoothLimit.Space), (A x) ((B x) v) = v) (u : ↥EulerMeanSolenoidal.L2) : (multiplier A) ((multiplier B) u) = u

theorem EulerMeanCoefficients.multiplier_adjoint (A B : Field) (hB : ∀ (x : EulerSmoothLimit.Space), B x = ContinuousLinearMap.adjoint (A x)) : multiplier B = ContinuousLinearMap.adjoint (multiplier A)

theorem EulerMeanCoefficients.multiplier_eq_coefficientOperator (A : Field) (C : NNReal) (hC : ∀ (x : EulerSmoothLimit.Space), ‖A x‖ ≤ ↑C) : multiplier A = EulerLiftedPressure.coefficientOperator ⇑A ⋯ C hC

theorem EulerMeanCoefficients.multiplier_quadratic_upper (A : Field) (K : ℝ) (hA : ∀ (x v : EulerSmoothLimit.Space), inner ℝ ((A x) v) v ≤ K * ‖v‖ ^ 2) (u : ↥EulerMeanSolenoidal.L2) : inner ℝ ((multiplier A) u) u ≤ K * ‖u‖ ^ 2