Documentation

LeanPool.NavierStokesAndEuler.Euler.TimeLpCoefficientGevrey

Quantitative parameter derivatives of time multipliers #

The Bochner multiplier is a linear contraction of the uniform coefficient path. These are bounds on genuine parameter derivatives of that operator, including the H¹ moving-frame transport used in the variational inverse.

source
@[instance_reducible]
noncomputable def EulerTimeLpCoefficientGevrey.coefficientPathGroup {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) :
NormedAddCommGroup C(↑(Set.Icc 0 T), E →L[ℝ] F)

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

Equations
Instances For
    source
    @[instance_reducible]
    noncomputable def EulerTimeLpCoefficientGevrey.coefficientPathSpace {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) :
    NormedSpace ℝ C(↑(Set.Icc 0 T), E →L[ℝ] F)

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

    Equations
    Instances For
      source
      @[instance_reducible]
      noncomputable def EulerTimeLpCoefficientGevrey.timeOperatorGroup {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) :
      NormedAddCommGroup (↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T F))

      Cache the standard NormedAddCommGroup (TimeLp T E →L[ℝ] TimeLp T F) instance to shorten typeclass synthesis.

      Equations
      Instances For
        source
        @[instance_reducible]
        noncomputable def EulerTimeLpCoefficientGevrey.timeOperatorSpace {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) :
        NormedSpace ℝ (↥(EulerTimeLp.TimeLp T E) →L[ℝ] ↥(EulerTimeLp.TimeLp T F))

        Cache the standard NormedSpace ℝ (TimeLp T E →L[ℝ] TimeLp T F) instance to shorten typeclass synthesis.

        Equations
        Instances For
          source
          theorem EulerTimeLpCoefficientGevrey.coefficientMap_norm {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) :
          ‖EulerTimeLpCoefficientMap.coefficientMap T hT‖ ≤ 1

          The actual coefficient-to-multiplier map is a linear contraction.

          source
          theorem EulerTimeLpCoefficientGevrey.primitive_norm_le_time {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) :
          ‖EulerTerminalTimePrimitive.primitiveTimeLp T hT‖ ≤ T

          A convenient polynomial bound for the genuine terminal primitive.

          source
          theorem EulerTimeLpCoefficientGevrey.timeMultiplier_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : P → C(↑(Set.Icc 0 T), E →L[ℝ] F)) (hA : ContDiff ℝ (↑⊤) A) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (d : ℕ) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R d n) (n : ℕ) (x : P) :
          ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTimeLp.timeMultiplier T hT (A y)) x‖ ≤ C * EulerGevrey.majorant R d n

          Actual multiplier derivatives retain the coefficient factorial bounds.

          source
          theorem EulerTimeLpCoefficientGevrey.productDerivative_bound {P : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A B : P → C(↑(Set.Icc 0 T), E →L[ℝ] F)) (hA : ContDiff ℝ (↑⊤) A) (hB : ContDiff ℝ (↑⊤) B) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (d : ℕ) (ha : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ C * EulerGevrey.majorant R d n) (hb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n B x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) :
          ‖iteratedFDeriv ℝ n (fun (y : P) => EulerTimeH1OperatorProduct.productDerivative T hT (A y) (B y)) x‖ ≤ (T * D + C) * EulerGevrey.majorant R d n

          The genuine H¹ transport costs only the polynomial factor from terminal integration.