Same-radius word bounds on the actual raw-field witnesses used by the packet recursion.

Fixed bounded vector operations preserve the genuine nonlinear H6 word estimates.

@[instance_reducible]

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

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

Equations

• EulerCylinderPathProduct.instCylinderPathBilinearBounds1 P = inferInstance

@[instance_reducible]

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

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

Equations

• EulerCylinderPathProduct.instCylinderPathBilinearBounds2 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathBilinearBounds3 (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

• EulerCylinderPathProduct.instCylinderPathBilinearBounds3 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderPathProduct.instCylinderPathBilinearBounds4 (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

• EulerCylinderPathProduct.instCylinderPathBilinearBounds4 P = inferInstance

theorem EulerCylinderPathProduct.pathMap_block_le (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (q n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) ((EulerCylinderConstantMap.pathMap P A) p)) n a ≤ ‖A‖ * EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a

theorem EulerCylinderPathProduct.bilinearProductPath_majorant (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (B : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hC : 0 ≤ C) (d e : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a ≤ A * EulerGevrey.majorant R d n) (hc : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) q) n a ≤ C * EulerGevrey.majorant R e n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (bilinearProductPath P B p q hp hq)) n a ≤ 9 * productBlockConstant P * ‖B‖ * A * C * EulerGevrey.majorant R (d + e) n

The field word radius is unchanged by an arbitrary fixed bounded bilinear vector map.

def EulerPacketCylinderField.Field.WordBound {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} (G : Field P T raw) (q : ℕ) (R A : ℝ) (d : ℕ) : Prop

Word bound, given by ∀ n, block standardDirection q (fun a : LiftTangent => pathTranslate P a G.path) n 0 ≤ A*majorant R d n.

Equations

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

theorem EulerPacketCylinderField.Field.WordBound.transfer {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (h : G.WordBound q R A d) (H : Field P T raw) : H.WordBound q R A d

theorem EulerPacketCylinderField.Field.WordBound.congr {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (h : G.WordBound q R A d) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw' (↑t, x, θ) = raw (↑t, x, θ)) : (G.congr he).WordBound q R A d

theorem EulerPacketCylinderField.Field.WordBound.mono_amplitude {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A B : ℝ} (h : G.WordBound q R A d) (hR : 0 ≤ R) (hAB : A ≤ B) : G.WordBound q R B d

theorem EulerPacketCylinderField.Field.WordBound.mono_shift {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d e : ℕ} {R A : ℝ} (h : G.WordBound q R A d) (hR : 1 ≤ R) (hA : 0 ≤ A) (hde : d ≤ e) : G.WordBound q R A e

theorem EulerPacketCylinderField.Field.wordBound_zero (P T : ℝ) [Fact (0 < P)] (q : ℕ) (R : ℝ) (d : ℕ) : (zero P T).WordBound q R 0 d

theorem EulerPacketCylinderField.Field.WordBound.add {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} {q d : ℕ} {R A B : ℝ} (hG : G.WordBound q R A d) (hH : H.WordBound q R B d) : (G.add H).WordBound q R (A + B) d

theorem EulerPacketCylinderField.Field.WordBound.sub {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} {q d : ℕ} {R A B : ℝ} (hG : G.WordBound q R A d) (hH : H.WordBound q R B d) : (G.sub H).WordBound q R (A + B) d

theorem EulerPacketCylinderField.Field.WordBound.smul {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (c : ℝ) : (G.smul c).WordBound q R (|c| * A) d

theorem EulerPacketCylinderField.Field.WordBound.neg {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) : G.neg.WordBound q R A d

theorem EulerPacketCylinderField.Field.WordBound.derivative {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (i : Fin 4) : (G.derivative i).WordBound q R A (d + 1)

theorem EulerPacketCylinderField.Field.WordBound.map {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : (G.map L).WordBound q R (‖L‖ * A) d

theorem EulerPacketCylinderField.Field.wordBound_finsetSum {P T : ℝ} [Fact (0 < P)] {q d : ℕ} {R : ℝ} {ι : Type u_1} (s : Finset ι) (f : ι → EulerPacketProfileRecursion.VectorField) (G : (i : ι) → Field P T (f i)) (A : ι → ℝ) (h : ∀ i ∈ s, (G i).WordBound q R (A i) d) : (finsetSum s f G).WordBound q R (∑ i ∈ s, A i) d

theorem EulerPacketCylinderField.Field.WordBound.scalarProduct {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} {d e : ℕ} {R A B : ℝ} (hG : G.WordBound 6 R A d) (hH : H.WordBound 6 R B e) (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) : (G.scalarProduct H L hL).WordBound 6 R (3 * EulerCylinderPathProduct.productBlockConstant P * A * B) (d + e)

theorem EulerPacketCylinderField.Field.WordBound.bilinear {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} {d e : ℕ} {R A B : ℝ} (hG : G.WordBound 6 R A d) (hH : H.WordBound 6 R B e) (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) : (G.bilinear H L).WordBound 6 R (9 * EulerCylinderPathProduct.productBlockConstant P * ‖L‖ * A * B) (d + e)

theorem EulerPacketCylinderField.Field.WordBound.spatialTransport {P T : ℝ} [Fact (0 < P)] {raw raw' : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {H : Field P T raw'} {d e : ℕ} {R A B : ℝ} (hG : G.WordBound 6 R A d) (hH : H.WordBound 6 R B e) (hR : 0 ≤ R) (hA : 0 ≤ A) (hB : 0 ≤ B) : (G.spatialTransport H).WordBound 6 R (9 * EulerCylinderPathProduct.productBlockConstant P * A * B) (d + e + 1)

theorem EulerPacketCylinderField.Field.WordBound.multiply {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q d : ℕ} {R A : ℝ} (hG : G.WordBound q R A d) {coef : EulerPacketPointJets.Domain → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space} (K : MatrixCoefficient T coef) (Rc C : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hA : 0 ≤ A) (hR : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) Rc ≤ R) (hK : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath K.path) a‖ ≤ C * EulerGevrey.majorant Rc 0 n) : (K.multiply G).WordBound q R (3 * EulerParameterWordGevrey.sobolevCoefficientAmplitude (Fin 4) q Rc C * A) d