Documentation

LeanPool.NavierStokesAndEuler.Euler.MeanFixedTranslation

Spatial translation covariance of the actual fixed mean form #

The full form, including its nonlocal initial boundary operator, transforms by ordinary spatial translation. Consequently its coercivity persists with the same constant throughout the translated coefficient family.

source
@[instance_reducible]
noncomputable def EulerMeanFixedTranslation.instMeanFixedTranslation1 :
NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable def EulerMeanFixedTranslation.instMeanFixedTranslation2 :
    InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

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

    Equations
    Instances For
      source
      @[instance_reducible]
      noncomputable def EulerMeanFixedTranslation.instMeanFixedTranslation3 (T : ℝ) :
      NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

      Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

      Equations
      Instances For
        source
        @[instance_reducible]
        noncomputable def EulerMeanFixedTranslation.instMeanFixedTranslation4 (T : ℝ) :
        InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

        Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

        Equations
        Instances For
          source
          @[instance_reducible]
          noncomputable def EulerMeanFixedTranslation.instMeanFixedTranslation5 (T : ℝ) :
          NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

          Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

          Equations
          Instances For
            source
            @[instance_reducible]
            noncomputable def EulerMeanFixedTranslation.instMeanFixedTranslation6 (T : ℝ) :
            InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

            Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

            Equations
            Instances For
              source
              noncomputable def EulerMeanFixedTranslation.translatedMeanOperator (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) :
              ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

              The fixed mean operator with genuinely translated spatial coefficients.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def EulerMeanFixedTranslation.translatedMeanPrimitive (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) :
                ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →L[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

                The physical primitive map with genuinely translated coefficients.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem EulerMeanFixedTranslation.fixedMeanDerivative_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) :
                  (EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT (EulerMeanOperatorTranslation.translatePath T a F) (EulerMeanOperatorTranslation.translatePath T a F₁)) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) u) = (EulerMeanTimeTranslation.timeTranslation T a) ((EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT F F₁) u)

                  Covariance of the actual physical derivative.

                  source
                  theorem EulerMeanFixedTranslation.fixedMeanPrimitive_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) :
                  (translatedMeanPrimitive T hT a F F₁) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) u) = (EulerMeanTimeTranslation.timeTranslation T a) ((EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁) u)

                  Covariance of the actual physical primitive.

                  source
                  theorem EulerMeanFixedTranslation.fixedMeanTrace_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) :
                  (EulerMeanFixedSpaceInverse.fixedMeanTrace T hT (EulerMeanOperatorTranslation.translatePath T a F) (EulerMeanOperatorTranslation.translatePath T a F₁)) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) u) = (EulerMeanSolenoidal.translation a) ((EulerMeanFixedSpaceInverse.fixedMeanTrace T hT F F₁) u)

                  Covariance includes the actual initial trace.

                  source
                  theorem EulerMeanFixedTranslation.boundaryCoefficient_translate (a : EulerSmoothLimit.Space) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (u : ↥EulerMeanSolenoidal.L2) :
                  (EulerMeanOperatorTranslation.translateOperator a M0 + L • EulerMeanOperatorTranslation.translateOperator a A) ((EulerMeanSolenoidal.translation a) u) = (EulerMeanSolenoidal.translation a) ((M0 + L • A) u)

                  The two actual initial boundary terms transform together.

                  source
                  theorem EulerMeanFixedTranslation.fixedMeanForm_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (u v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) :
                  inner ℝ ((translatedMeanOperator T hT a F F₁ H M0 A L) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) u)) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) = inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) u) v

                  The whole physical bilinear form is invariant under simultaneous translation.

                  source
                  theorem EulerMeanFixedTranslation.eq_of_translated_pairing (T : ℝ) (a : EulerSmoothLimit.Space) (x y : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (h : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), inner ℝ x ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v) = inner ℝ y ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) v)) :
                  x = y

                  Testing after every spatial translation still determines a Hilbert vector.

                  source
                  theorem EulerMeanFixedTranslation.fixedMeanOperator_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) :
                  (translatedMeanOperator T hT a F F₁ H M0 A L) ((EulerMeanTimeTranslation.timeSolenoidalTranslation T a) u) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) u)

                  Covariance is an equality of the actual fixed-space bounded operators.

                  source
                  theorem EulerMeanFixedTranslation.translatedMeanOperator_coercive (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L c : ℝ) (hcoercive : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) :
                  c * ‖v‖ ^ 2 ≤ inner ℝ ((translatedMeanOperator T hT a F F₁ H M0 A L) v) v

                  The same positive coercivity constant holds for all genuinely translated coefficients.

                  source
                  theorem EulerMeanFixedTranslation.fixedMeanPrimitive_adjoint_translate (T : ℝ) (hT : 0 ≤ T) (a : EulerSmoothLimit.Space) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) :
                  (ContinuousLinearMap.adjoint (translatedMeanPrimitive T hT a F F₁)) ((EulerMeanTimeTranslation.timeTranslation T a) f) = (EulerMeanTimeTranslation.timeSolenoidalTranslation T a) ((ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) f)

                  The forcing adjoint transforms by the same actual spatial action.