Exact profile normalization of spatial derivative paths and the vector potential.

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialWeight1 (P : ℝ) [Fact (0 < P)] : NormedAddCommGroup ↥(EulerLiftedGradientSpace.LiftL2 P)

Cache the standard NormedAddCommGroup (LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPotential.instCylinderPotentialWeight1 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialWeight2 (P : ℝ) [Fact (0 < P)] : NormedSpace ℝ ↥(EulerLiftedGradientSpace.LiftL2 P)

Cache the standard NormedSpace ℝ (LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPotential.instCylinderPotentialWeight2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialWeight3 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedAddCommGroup C(K,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPotential.instCylinderPotentialWeight3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialWeight4 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedSpace ℝ C(K,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPotential.instCylinderPotentialWeight4 P = inferInstance

theorem EulerCylinderPotential.weighted_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.weight g) p)

theorem EulerCylinderPotential.wordPath_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) {n : ℕ} (w : Fin n → Fin 4) : EulerCylinderSmoothOrbit.wordPath P ((EulerContinuousTimeWeight.weight g) p) w = (EulerContinuousTimeWeight.weight g) (EulerCylinderSmoothOrbit.wordPath P p w)

The entire spatial/angular word commutes with a time-only scalar factor.

theorem EulerCylinderPotential.derivativePath_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (i : Fin 4) : EulerCylinderSmoothOrbit.derivativePath P ((EulerContinuousTimeWeight.weight g) p) i = (EulerContinuousTimeWeight.weight g) (EulerCylinderSmoothOrbit.derivativePath P p i)

theorem EulerCylinderPotential.pathPrimitive_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) : (EulerCylinderAnglePrimitive.pathPrimitive P) ((EulerContinuousTimeWeight.weight g) p) = (EulerContinuousTimeWeight.weight g) ((EulerCylinderAnglePrimitive.pathPrimitive P) p)

theorem EulerCylinderPotential.fullMultiplier_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) : ((EulerLpCylinderRectangular.fullMultiplierMap P) B) ((EulerContinuousTimeWeight.weight g) p) = (EulerContinuousTimeWeight.weight g) (((EulerLpCylinderRectangular.fullMultiplierMap P) B) p)

theorem EulerCylinderPotential.potentialPath_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) : potentialPath P B ((EulerContinuousTimeWeight.weight g) p) = (EulerContinuousTimeWeight.weight g) (potentialPath P B p)

theorem EulerCylinderPotential.potentialPath_normalize (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hg : ∀ (t : K), 0 < g t) : potentialPath P B ((EulerContinuousTimeWeight.normalize g hg) p) = (EulerContinuousTimeWeight.normalize g hg) (potentialPath P B p)

theorem EulerCylinderPotential.normalized_potentialPath_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (B : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hg : ∀ (t : K), 0 < g t) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) p)) {ι : Type u_2} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (Rc C R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R) (hbB : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath B) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbp : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) p)) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (potentialPath P B p))) n 0 ≤ 3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C * (P * D) * EulerGevrey.majorant R d n

The bound applies to the literal quotient Q/g, without any extrema or derivative of g.