Translation derivatives and actual weak derivatives on the lifted cylinder. Smooth compact test fields are realized in L², and their translation orbits are differentiated in the strong L² topology.

@[instance_reducible]

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

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

Equations

• EulerLiftedWeakDerivative.coefficientValueNormedGroup = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

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

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

Equations

• EulerLiftedWeakDerivative.coefficientValueNormedSpace = ContinuousLinearMap.toNormedSpace

@[instance_reducible]

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

The existing Mathlib normed group instance for first coefficient derivatives.

Equations

• EulerLiftedWeakDerivative.coefficientFirstNormedGroup = ContinuousLinearMap.toNormedAddCommGroup

@[instance_reducible]

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

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

Equations

• EulerLiftedWeakDerivative.coefficientFirstNormedSpace = ContinuousLinearMap.toNormedSpace

noncomputable def EulerLiftedWeakDerivative.fieldFDeriv (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.LiftTangent →L[ℝ] W

The full derivative of a field in covering coordinates, evaluated at the center.

Equations

• EulerLiftedWeakDerivative.fieldFDeriv period f x = fderiv ℝ (EulerMetricTransport.localFieldLift period f x) 0

theorem EulerLiftedWeakDerivative.localFieldLift_fieldFDeriv (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerMetricTransport.localFieldLift period (fieldFDeriv period f) x = fderiv ℝ (EulerMetricTransport.localFieldLift period f x)

theorem EulerLiftedWeakDerivative.fieldFDeriv_smooth (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (fieldFDeriv period f) x)

theorem EulerLiftedWeakDerivative.fieldFDeriv_zero_outside (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (x : EulerLiftedGradientSpace.LiftDomain period) (hx : x ∉ tsupport f) : fieldFDeriv period f x = 0

theorem EulerLiftedWeakDerivative.fieldFDeriv_compact (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (hf : HasCompactSupport f) : HasCompactSupport (fieldFDeriv period f)

theorem EulerLiftedWeakDerivative.fieldDerivative_compact (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (hf : HasCompactSupport f) : HasCompactSupport (EulerTransportDerivatives.fieldDerivative period a f)

theorem EulerLiftedWeakDerivative.fieldDerivative_memLp (period : ℝ) [Fact (0 < period)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → W) (hfc : HasCompactSupport f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : MeasureTheory.MemLp (EulerTransportDerivatives.fieldDerivative period a f) 2 (EulerLiftedGradientSpace.liftMeasure period)

theorem EulerLiftedWeakDerivative.compact_smooth_second_derivative_bound (period : ℝ) {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftDomain period → W) (hfc : HasCompactSupport f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : ∃ (M : NNReal), ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (y : EulerLiftedGradientSpace.LiftTangent), ‖fderiv ℝ (fderiv ℝ (EulerMetricTransport.localFieldLift period f x)) y‖ ≤ ↑M

theorem EulerLiftedWeakDerivative.translationPath_continuous (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) : Continuous (EulerPressureSpatialRegularity.translationPath period a)

theorem EulerLiftedWeakDerivative.translationPath_add (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (s t : ℝ) : EulerPressureSpatialRegularity.translationPath period a (s + t) = EulerPressureSpatialRegularity.translationPath period a s + EulerPressureSpatialRegularity.translationPath period a t

theorem EulerLiftedWeakDerivative.translationPath_neg (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerPressureSpatialRegularity.translationPath period a (-t) = -EulerPressureSpatialRegularity.translationPath period a t

theorem EulerLiftedWeakDerivative.translation_pairing (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftDomain period) (f g : ↥(EulerLiftedGradientSpace.LiftL2 period)) : inner ℝ ((EulerLiftedGradientSpace.translation period a) f) g = inner ℝ f ((EulerLiftedGradientSpace.translation period (-a)) g)

theorem EulerLiftedWeakDerivative.compact_translation_support (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hfc : HasCompactSupport f) : ∃ (K : Set (EulerLiftedGradientSpace.LiftDomain period)), IsCompact K ∧ tsupport f ⊆ K ∧ ∀ (t : ℝ), |t| ≤ 1 → ∀ x ∉ K, f (x + EulerPressureSpatialRegularity.translationPath period a t) = 0

noncomputable def EulerLiftedWeakDerivative.smoothFieldLp (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hfc : HasCompactSupport f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual L² element represented by a smooth compact vector field.

Equations

• EulerLiftedWeakDerivative.smoothFieldLp period f hfc hf = MeasureTheory.MemLp.toLp f ⋯

theorem EulerLiftedWeakDerivative.smoothFieldLp_ae (period : ℝ) [Fact (0 < period)] (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hfc : HasCompactSupport f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : ↑↑(smoothFieldLp period f hfc hf) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f

noncomputable def EulerLiftedWeakDerivative.derivativeFieldLp (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hfc : HasCompactSupport f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The L² element represented by the actual directional derivative of a compact test field.

Equations

• EulerLiftedWeakDerivative.derivativeFieldLp period a f hfc hf = MeasureTheory.MemLp.toLp (EulerTransportDerivatives.fieldDerivative period a f) ⋯

theorem EulerLiftedWeakDerivative.derivativeFieldLp_ae (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hfc : HasCompactSupport f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : ↑↑(derivativeFieldLp period a f hfc hf) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerTransportDerivatives.fieldDerivative period a f

theorem EulerLiftedWeakDerivative.field_translation_remainder (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (M : NNReal) (hDD : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (y : EulerLiftedGradientSpace.LiftTangent), ‖fderiv ℝ (fderiv ℝ (EulerMetricTransport.localFieldLift period f x)) y‖ ≤ ↑M) (t : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : ‖f (x + EulerPressureSpatialRegularity.translationPath period a t) - f x - t • EulerTransportDerivatives.fieldDerivative period a f x‖ ≤ ↑M * ‖a‖ ^ 2 * |t| ^ 2

theorem EulerLiftedWeakDerivative.smoothFieldLp_translation_hasDerivAt (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hfc : HasCompactSupport f) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) (smoothFieldLp period f hfc hf)) (derivativeFieldLp period a f hfc hf) 0

theorem EulerLiftedWeakDerivative.translation_derivative_pairing (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f f' g g' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) (hg : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) g) g' 0) : inner ℝ f' g = -inner ℝ f g'

theorem EulerLiftedWeakDerivative.strong_translation_derivative_weak (period : ℝ) [Fact (0 < period)] (a : EulerLiftedGradientSpace.LiftTangent) (f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)) (hf : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) (φ : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hφc : HasCompactSupport φ) (hφ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period φ x)) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ (↑↑f' x) (φ x) ∂EulerLiftedGradientSpace.liftMeasure period = -∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ (↑↑f x) (EulerTransportDerivatives.fieldDerivative period a φ x) ∂EulerLiftedGradientSpace.liftMeasure period

A strong L² translation derivative is the actual distributional derivative.

theorem EulerLiftedWeakDerivative.divergenceFree_translation_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (a : EulerLiftedGradientSpace.LiftDomain period) {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hf : f ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) : (EulerLiftedGradientSpace.translation period a) f ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

theorem EulerLiftedWeakDerivative.divergenceFree_translation_derivative (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (a : EulerLiftedGradientSpace.LiftTangent) {f f' : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hf : f ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) (hder : HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) : f' ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

theorem EulerLiftedWeakDerivative.pressure_has_weak_derivative (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 (EulerPressureSpatialRegularity.translationPath period a t)) f) f' 0) : ∃ (p' : ↥(EulerLiftedGradientSpace.LiftL2 period)), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period a t)) (EulerPressureSpatialRegularity.liftedPressure period κ m A hA C hAb c hc hpos f)) p' 0 ∧ p' ∈ EulerLiftedGradientSpace.gradientSpace period κ m ∧ ‖p'‖ ≤ c⁻¹ * (‖f'‖ + ↑D * ‖a‖ * ‖EulerPressureSpatialRegularity.liftedPressure period κ m A hA C hAb c hc hpos f‖) ∧ ∀ (φ : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), HasCompactSupport φ → (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period φ x)) → ∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ (↑↑p' x) (φ x) ∂EulerLiftedGradientSpace.liftMeasure period = -∫ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ (↑↑(EulerPressureSpatialRegularity.liftedPressure period κ m A hA C hAb c hc hpos f) x) (EulerTransportDerivatives.fieldDerivative period a φ x) ∂EulerLiftedGradientSpace.liftMeasure period