Related estimates used together by the same construction modules.

Exact time-profile normalization of the actual slow curl and its time derivative.

@[instance_reducible]

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

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlWeight1 P = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurlWeight2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlWeight3 (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

• EulerCylinderSlowCurl.instCylinderSlowCurlWeight3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurlWeight4 (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

• EulerCylinderSlowCurl.instCylinderSlowCurlWeight4 P = inferInstance

theorem EulerCylinderSlowCurl.term_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (i : Fin 3) : term P G ((EulerContinuousTimeWeight.weight g) p) i = (EulerContinuousTimeWeight.weight g) (term P G p i)

theorem EulerCylinderSlowCurl.path_weight (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : path P G ((EulerContinuousTimeWeight.weight g) p) = (EulerContinuousTimeWeight.weight g) (path P G p)

theorem EulerCylinderSlowCurl.path_normalize (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hg : ∀ (t : K), 0 < g t) : path P G ((EulerContinuousTimeWeight.normalize g hg) p) = (EulerContinuousTimeWeight.normalize g hg) (path P G p)

theorem EulerCylinderSlowCurl.normalized_path_block_bound (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (g : C(K, ℝ)) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hg : ∀ (t : K), 0 < g t) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (q : ℕ) (Rc C R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hbG : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath G) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbp : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 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 EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (path P G p))) n 0 ≤ 9 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * D * EulerGevrey.majorant R (d + 1) n

The literal normalized curl has the same radius, with one spatial derivative.

theorem EulerCylinderSlowCurl.derivative_normalize (P : ℝ) [Fact (0 < P)] (T : ℝ) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (G G₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) : (EulerContinuousTimeWeight.normalize g hg) (derivative P T G G₁ p f) = derivative P T G G₁ ((EulerContinuousTimeWeight.normalize g hg) p) ((EulerContinuousTimeWeight.normalize g hg) f)

This is C_t/g, so no derivative or extremum of the profile is needed.

theorem EulerCylinderSlowCurl.normalized_derivative_block_bound (P : ℝ) [Fact (0 < P)] (T : ℝ) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) (G G₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (hG₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G₁)) (q : ℕ) (Rc C R D : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hD : 0 ≤ D) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hbG : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath G) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (hbG₁ : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath G₁) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) (d : ℕ) (hbp : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) p)) n 0 ≤ D * EulerGevrey.majorant R d n) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) f)) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) (derivative P T G G₁ p f))) n 0 ≤ 18 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * D * EulerGevrey.majorant R (d + 1) n

Same-radius bounds and literal profile normalization for the constructed potential time derivative.

@[instance_reducible]

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

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

Equations

• EulerCylinderPotential.instCylinderPotentialTimeWeight1 P = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCylinderPotential.instCylinderPotentialTimeWeight2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialTimeWeight3 (P : ℝ) [Fact (0 < P)] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPotential.instCylinderPotentialTimeWeight3 P T = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPotential.instCylinderPotentialTimeWeight4 (P : ℝ) [Fact (0 < P)] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderPotential.instCylinderPotentialTimeWeight4 P T = inferInstance

theorem EulerCylinderPotential.potentialDerivative_block_bound (P : ℝ) [Fact (0 < P)] (T : ℝ) (B B₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (hB₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B₁)) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) {ι : Type u_1} [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) (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) p) n 0 ≤ D * EulerGevrey.majorant R d n) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) n 0 ≤ D * EulerGevrey.majorant R d n) (n : ℕ) : EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (potentialDerivative P T B B₁ p f)) n 0 ≤ 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C * (P * D) * EulerGevrey.majorant R d n

theorem EulerCylinderPotential.potentialDerivative_normalize (P : ℝ) [Fact (0 < P)] (T : ℝ) (B B₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) : (EulerContinuousTimeWeight.normalize g hg) (potentialDerivative P T B B₁ p f) = potentialDerivative P T B B₁ ((EulerContinuousTimeWeight.normalize g hg) p) ((EulerContinuousTimeWeight.normalize g hg) f)

theorem EulerCylinderPotential.normalized_potentialDerivative_block_bound (P : ℝ) [Fact (0 < P)] (T : ℝ) (B B₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hB : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B)) (hB₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath B₁)) (p f : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hf : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) f) (g : C(↑(Set.Icc 0 T), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 T)), 0 < g t) {ι : Type u_1} [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) (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) (hbf : ∀ (n : ℕ), EulerParameterWordGevrey.block directions q (fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) ((EulerContinuousTimeWeight.normalize g hg) f)) 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) (potentialDerivative P T B B₁ p f))) n 0 ≤ 6 * EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q Rc C * (P * D) * EulerGevrey.majorant R d n

Estimate Q_t/g from A/g and A_t/g, without differentiating the profile g.