Compact smooth fields have actual smooth mixed L² translation orbits

This is a full Fréchet derivative in the four-dimensional covering space. The compact support argument controls every small covering translation, including its angular component, before dominated L² differentiation.

structure EulerCylinderCompact.CompactField (P : ℝ) (V : Type u) [NormedAddCommGroup V] [NormedSpace ℝ V] : Type u

Compact field data, collecting field, compact, smooth.

• field : EulerLiftedGradientSpace.LiftDomain P → V

  Underlying field of CompactField, of type LiftDomain P → V.

• compact : HasCompactSupport self.field
• smooth (x : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P self.field x)

theorem EulerCylinderCompact.CompactField.continuous {P : ℝ} {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : Continuous A.field

noncomputable def EulerCylinderCompact.CompactField.toLp {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : ↥(EulerLpCylinderTranslation.CylinderL2 P V)

To Lᵖ, given by (A.continuous.memLp_of_hasCompactSupport A.compact).toLp A.field.

Equations

• A.toLp = MeasureTheory.MemLp.toLp A.field ⋯

theorem EulerCylinderCompact.CompactField.toLp_ae {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : ↑↑A.toLp =ᵐ[EulerLiftedGradientSpace.liftMeasure P] A.field

noncomputable def EulerCylinderCompact.CompactField.derivative {P : ℝ} {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : CompactField P (EulerLiftedGradientSpace.LiftTangent →L[ℝ] V)

Derivative, bundling field, compact, smooth.

Equations

• A.derivative = { field := EulerLiftedWeakDerivative.fieldFDeriv P A.field, compact := ⋯, smooth := ⋯ }

theorem EulerCylinderCompact.CompactField.derivative_bound {P : ℝ} {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain P) (a : EulerLiftedGradientSpace.LiftTangent), ‖fderiv ℝ (EulerMetricTransport.localFieldLift P A.field x) a‖ ≤ C

theorem EulerCylinderCompact.CompactField.translation_support {P : ℝ} {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : ∃ (K : Set (EulerLiftedGradientSpace.LiftDomain P)), IsCompact K ∧ tsupport A.field ⊆ K ∧ ∀ (a : EulerLiftedGradientSpace.LiftTangent), ‖a‖ ≤ 1 → ∀ x ∉ K, A.field (x + EulerLiftedGradientSpace.coveringMap P a) = 0

One compact set contains every translate by a covering vector of norm at most one.

theorem EulerCylinderCompact.CompactField.increment_bound {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : ∃ (M : EulerLiftedGradientSpace.LiftDomain P → ℝ), MeasureTheory.MemLp M 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (∀ (x : EulerLiftedGradientSpace.LiftDomain P), 0 ≤ M x) ∧ ∀ (a : EulerLiftedGradientSpace.LiftTangent), ‖a‖ ≤ 1 → ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ‖A.field (x + EulerLiftedGradientSpace.coveringMap P a) - A.field x‖ ≤ M x * ‖a‖

theorem EulerCylinderCompact.CompactField.hasFDerivAt_zero {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : HasFDerivAt (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) A.toLp) (EulerLpDerivative.derivativeMap (EulerLiftedGradientSpace.liftMeasure P) A.derivative.toLp) 0

theorem EulerCylinderCompact.CompactField.derivativeMap_translation {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (D : ↥(EulerLpCylinderTranslation.CylinderL2 P (EulerLiftedGradientSpace.LiftTangent →L[ℝ] V))) (a : EulerLiftedGradientSpace.LiftTangent) : EulerLpDerivative.derivativeMap (EulerLiftedGradientSpace.liftMeasure P) ((EulerLpCylinderTranslation.translate P a) D) = (EulerLpCylinderTranslation.translate P a).toContinuousLinearMap ∘SL EulerLpDerivative.derivativeMap (EulerLiftedGradientSpace.liftMeasure P) D

theorem EulerCylinderCompact.CompactField.translation_hasFDerivAt {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) (a : EulerLiftedGradientSpace.LiftTangent) : HasFDerivAt (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P b) A.toLp) (EulerLpDerivative.derivativeMap (EulerLiftedGradientSpace.liftMeasure P) ((EulerLpCylinderTranslation.translate P a) A.derivative.toLp)) a

theorem EulerCylinderCompact.CompactField.translation_fderiv {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : (fderiv ℝ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) A.toLp) = fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpDerivative.derivativeBundling (EulerLiftedGradientSpace.liftMeasure P)) ((EulerLpCylinderTranslation.translate P a) A.derivative.toLp)

theorem EulerCylinderCompact.CompactField.translation_contDiff {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) A.toLp

All four covering directions are differentiated in the actual L² norm.