Spatial pressure regularity in the genuine lifted L² space. Coefficient translations are actual pointwise translations, and pressure translation covariance follows from the uniquely constructed projected equation.

@[instance_reducible]

noncomputable def EulerPressureSpatialRegularity.coefficientValueNormedGroup : NormedAddCommGroup (EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib normed group instance for matrix coefficients, named to keep inference shallow.

Equations

• EulerPressureSpatialRegularity.coefficientValueNormedGroup = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable def EulerPressureSpatialRegularity.coefficientValueNormedSpace : NormedSpace ℝ (EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib real normed-space instance for matrix coefficients.

Equations

• EulerPressureSpatialRegularity.coefficientValueNormedSpace = ContinuousLinearMap.toNormedSpace

@[instance_reducible]

noncomputable def EulerPressureSpatialRegularity.coefficientFirstNormedGroup : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib normed group instance for first coefficient derivatives.

Equations

• EulerPressureSpatialRegularity.coefficientFirstNormedGroup = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

noncomputable def EulerPressureSpatialRegularity.coefficientFirstNormedSpace : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3)

The existing Mathlib real normed-space instance for first coefficient derivatives.

Equations

• EulerPressureSpatialRegularity.coefficientFirstNormedSpace = ContinuousLinearMap.toNormedSpace

theorem EulerPressureSpatialRegularity.coefficientOperator_remainder_norm {α : Type u_1} {V : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A B D : α → V →L[ℝ] V) (hA : MeasureTheory.AEStronglyMeasurable A μ) (hB : MeasureTheory.AEStronglyMeasurable B μ) (hD : MeasureTheory.AEStronglyMeasurable D μ) (CA CB CD R : NNReal) (hAb : ∀ (x : α), ‖A x‖ ≤ ↑CA) (hBb : ∀ (x : α), ‖B x‖ ≤ ↑CB) (hDb : ∀ (x : α), ‖D x‖ ≤ ↑CD) (t : ℝ) (hR : ∀ (x : α), ‖A x - B x - t • D x‖ ≤ ↑R) : ‖EulerLiftedPressure.coefficientOperator A hA CA hAb - EulerLiftedPressure.coefficientOperator B hB CB hBb - t • EulerLiftedPressure.coefficientOperator D hD CD hDb‖ ≤ ↑R

theorem EulerPressureSpatialRegularity.uniform_derivative_remainder {W : Type u_3} [NormedAddCommGroup W] [NormedSpace ℝ W] (f f' : ℝ → W) (hf : ∀ (s : ℝ), HasDerivAt f (f' s) s) (L : NNReal) (hL : ∀ (s : ℝ), ‖f' s - f' 0‖ ≤ ↑L * |s|) (t : ℝ) : ‖f t - f 0 - t • f' 0‖ ≤ ↑L * |t| ^ 2

theorem EulerPressureSpatialRegularity.coefficientOperator_hasDerivAt {α : Type u_1} {V : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (A A' : ℝ → α → V →L[ℝ] V) (hA : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (A t) μ) (hA' : MeasureTheory.AEStronglyMeasurable (A' 0) μ) (C D L : NNReal) (hAb : ∀ (t : ℝ) (x : α), ‖A t x‖ ≤ ↑C) (hDb : ∀ (x : α), ‖A' 0 x‖ ≤ ↑D) (hder : ∀ (t : ℝ) (x : α), HasDerivAt (fun (s : ℝ) => A s x) (A' t x) t) (hLip : ∀ (t : ℝ) (x : α), ‖A' t x - A' 0 x‖ ≤ ↑L * |t|) : HasDerivAt (fun (t : ℝ) => EulerLiftedPressure.coefficientOperator (A t) ⋯ C ⋯) (EulerLiftedPressure.coefficientOperator (A' 0) hA' D hDb) 0

theorem EulerPressureSpatialRegularity.directionalDerivative_line_lipschitz {V : Type u_1} {W : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] (f : V → W) (hf : ContDiff ℝ (↑⊤) f) (M : NNReal) (hDD : ∀ (x : V), ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ ↑M) (a : V) (t : ℝ) : ‖(fderiv ℝ f (t • a)) a - (fderiv ℝ f 0) a‖ ≤ ↑M * ‖a‖ ^ 2 * |t|

def EulerPressureSpatialRegularity.translatedCoefficient (period : ℝ) (a : EulerLiftedGradientSpace.LiftDomain period) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3

Pointwise coefficient translation on the actual cylinder.

Equations

• EulerPressureSpatialRegularity.translatedCoefficient period a A x = A (x + a)

theorem EulerPressureSpatialRegularity.translatedCoefficient_measurable (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftDomain period) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.AEStronglyMeasurable (translatedCoefficient period a A) (EulerLiftedGradientSpace.liftMeasure period)

def EulerPressureSpatialRegularity.translationPath (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerLiftedGradientSpace.LiftDomain period

The one-parameter spatial/angular translation determined by a covering-space direction.

Equations

• EulerPressureSpatialRegularity.translationPath period a t = EulerLiftedGradientSpace.coveringMap period (t • a)

@[simp]

theorem EulerPressureSpatialRegularity.translationPath_zero (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) : translationPath period a 0 = 0

noncomputable def EulerPressureSpatialRegularity.translatedCoefficientDerivative (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3

The actual directional derivative of the translated coefficient field.

Equations

• EulerPressureSpatialRegularity.translatedCoefficientDerivative period a A t x = (fderiv ℝ (EulerMetricTransport.localFieldLift period A x) (t • a)) a

theorem EulerPressureSpatialRegularity.translatedCoefficient_path (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : translatedCoefficient period (translationPath period a t) A x = EulerMetricTransport.localFieldLift period A x (t • a)

theorem EulerPressureSpatialRegularity.translatedCoefficient_hasDerivAt (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period A x)) (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : HasDerivAt (fun (s : ℝ) => translatedCoefficient period (translationPath period a s) A x) (translatedCoefficientDerivative period a A t x) t

theorem EulerPressureSpatialRegularity.translatedCoefficientDerivative_measurable (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period A x)) : MeasureTheory.AEStronglyMeasurable (translatedCoefficientDerivative period a A 0) (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerPressureSpatialRegularity.translatedCoefficientDerivative_bound (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (D : NNReal) (hD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period A x) 0‖ ≤ ↑D) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖translatedCoefficientDerivative period a A 0 x‖ ≤ ↑D * ‖a‖

theorem EulerPressureSpatialRegularity.translatedCoefficientDerivative_lipschitz (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period A x)) (M : NNReal) (hDD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (y : EulerLiftedGradientSpace.LiftTangent), ‖fderiv ℝ (fderiv ℝ (EulerMetricTransport.localFieldLift period A x)) y‖ ≤ ↑M) (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖translatedCoefficientDerivative period a A t x - translatedCoefficientDerivative period a A 0 x‖ ≤ ↑M * ‖a‖ ^ 2 * |t|

theorem EulerPressureSpatialRegularity.coefficientOperator_translation (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftDomain period) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerLiftedGradientSpace.translation period a) ((EulerLiftedPressure.coefficientOperator A hA C hAb) f) = (EulerLiftedPressure.coefficientOperator (translatedCoefficient period a A) ⋯ C ⋯) ((EulerLiftedGradientSpace.translation period a) f)

noncomputable def EulerPressureSpatialRegularity.liftedPressure (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The concrete coercive pressure solution, viewed in ambient L².

Equations

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

theorem EulerPressureSpatialRegularity.liftedPressure_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : liftedPressure period κ m A hA C hAb c hc hpos f ∈ EulerLiftedGradientSpace.gradientSpace period κ m

theorem EulerPressureSpatialRegularity.liftedPressure_equation (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerLiftedGradientSpace.gradientProjection period κ m) ((EulerLiftedPressure.coefficientOperator A hA C hAb) (liftedPressure period κ m A hA C hAb c hc hpos f)) = (EulerLiftedGradientSpace.gradientProjection period κ m) f

theorem EulerPressureSpatialRegularity.liftedPressure_unique (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f p : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hp : p ∈ EulerLiftedGradientSpace.gradientSpace period κ m) (heq : (EulerLiftedGradientSpace.gradientProjection period κ m) ((EulerLiftedPressure.coefficientOperator A hA C hAb) p) = (EulerLiftedGradientSpace.gradientProjection period κ m) f) : p = liftedPressure period κ m A hA C hAb c hc hpos f

theorem EulerPressureSpatialRegularity.liftedPressure_translation (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (a : EulerLiftedGradientSpace.LiftDomain period) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (C : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerLiftedGradientSpace.translation period a) (liftedPressure period κ m A hA C hAb c hc hpos f) = liftedPressure period κ m (translatedCoefficient period a A) ⋯ C ⋯ c hc ⋯ ((EulerLiftedGradientSpace.translation period a) f)

theorem EulerPressureSpatialRegularity.liftedPressure_hasDerivAt (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (A A' : ℝ → EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : ∀ (t : ℝ), MeasureTheory.AEStronglyMeasurable (A t) (EulerLiftedGradientSpace.liftMeasure period)) (hA' : MeasureTheory.AEStronglyMeasurable (A' 0) (EulerLiftedGradientSpace.liftMeasure period)) (C D L : NNReal) (hAb : ∀ (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period), ‖A t x‖ ≤ ↑C) (hDb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A' 0 x‖ ≤ ↑D) (hder : ∀ (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period), HasDerivAt (fun (s : ℝ) => A s x) (A' t x) t) (hLip : ∀ (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period), ‖A' t x - A' 0 x‖ ≤ ↑L * |t|) (c : ℝ) (hc : 0 < c) (hpos : ∀ (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A t x) v) v) (f : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 period)) (f' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt f f' 0) : HasDerivAt (fun (t : ℝ) => liftedPressure period κ m (A t) ⋯ C ⋯ c hc ⋯ (f t)) (liftedPressure period κ m (A 0) ⋯ C ⋯ c hc ⋯ (f' - (EulerLiftedPressure.coefficientOperator (A' 0) hA' D hDb) (liftedPressure period κ m (A 0) ⋯ C ⋯ c hc ⋯ (f 0)))) 0

theorem EulerPressureSpatialRegularity.pressure_translation_hasDerivAt (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (hAs : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period A x)) (C D M : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (hDA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period A x) 0‖ ≤ ↑D) (hDDA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (y : EulerLiftedGradientSpace.LiftTangent), ‖fderiv ℝ (fderiv ℝ (EulerMetricTransport.localFieldLift period A x)) y‖ ≤ ↑M) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (translationPath period a t)) f) f' 0) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (translationPath period a t)) (liftedPressure period κ m A hA C hAb c hc hpos f)) (liftedPressure period κ m A hA C hAb c hc hpos (f' - (EulerLiftedPressure.coefficientOperator (translatedCoefficientDerivative period a A 0) ⋯ (D * ‖a‖₊) ⋯) (liftedPressure period κ m A hA C hAb c hc hpos f))) 0

theorem EulerPressureSpatialRegularity.pressure_translation_derivative_norm (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (a : EulerLiftedGradientSpace.LiftTangent) (A : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.Vector3) (hA : MeasureTheory.AEStronglyMeasurable A (EulerLiftedGradientSpace.liftMeasure period)) (hAs : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period A x)) (C D M : NNReal) (hAb : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖A x‖ ≤ ↑C) (hDA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ‖fderiv ℝ (EulerMetricTransport.localFieldLift period A x) 0‖ ≤ ↑D) (hDDA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (y : EulerLiftedGradientSpace.LiftTangent), ‖fderiv ℝ (fderiv ℝ (EulerMetricTransport.localFieldLift period A x)) y‖ ≤ ↑M) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A x) v) v) (f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (translationPath period a t)) f) f' 0) : ‖deriv (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (translationPath period a t)) (liftedPressure period κ m A hA C hAb c hc hpos f)) 0‖ ≤ c⁻¹ * (‖f'‖ + ↑D * ‖a‖ * ‖liftedPressure period κ m A hA C hAb c hc hpos f‖)