The recursive physical state consists of the actual Euler solution, its all-order Sobolev fields, its particle-label bounds, and its symmetry. Restriction and the exact packet construction preserve these data.

Spatial Sobolev paths for the actual inverse parent flow. Its measure preservation, smoothness, derivative bounds and jet continuity are all derived from the source deformation and inverse identities.

Strong Sobolev continuity under genuine varying volume-preserving maps. Faà di Bruno gives actual derivative tensors, and dominated convergence handles the bounded, pointwise continuous coefficients.

Bounded pointwise operator fields act on actual L² classes. Joint continuity of the coefficients, with a uniform bound, gives strong continuity even when uniform convergence of coefficients is unavailable.

theorem EulerLpPointwiseMultiplier.apply_memLp {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) (u : ↥(MeasureTheory.Lp E 2 μ)) : MeasureTheory.MemLp (fun (x : X) => (A x) (↑↑u x)) 2 μ

noncomputable def EulerLpPointwiseMultiplier.applyLp {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) (u : ↥(MeasureTheory.Lp E 2 μ)) : ↥(MeasureTheory.Lp F 2 μ)

Apply Lᵖ, given by (apply_memLp μ A hA C hC u).toLp (fun x => A x (u x)).

Equations

• EulerLpPointwiseMultiplier.applyLp μ A hA C hC u = MeasureTheory.MemLp.toLp (fun (x : X) => (A x) (↑↑u x)) ⋯

theorem EulerLpPointwiseMultiplier.applyLp_ae {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) (u : ↥(MeasureTheory.Lp E 2 μ)) : ↑↑(applyLp μ A hA C hC u) =ᵐ[μ] fun (x : X) => (A x) (↑↑u x)

theorem EulerLpPointwiseMultiplier.applyLp_norm_le {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) (u : ↥(MeasureTheory.Lp E 2 μ)) : ‖applyLp μ A hA C hC u‖ ≤ C * ‖u‖

noncomputable def EulerLpPointwiseMultiplier.linear {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) : ↥(MeasureTheory.Lp E 2 μ) →ₗ[ℝ] ↥(MeasureTheory.Lp F 2 μ)

Linear, bundling toFun, map_add, map_smul.

Equations

• EulerLpPointwiseMultiplier.linear μ A hA C hC = { toFun := EulerLpPointwiseMultiplier.applyLp μ A hA C hC, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def EulerLpPointwiseMultiplier.operator {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) : ↥(MeasureTheory.Lp E 2 μ) →L[ℝ] ↥(MeasureTheory.Lp F 2 μ)

Operator, given by (linear μ A hA C hC).mkContinuous C (applyLp_norm_le μ A hA C hC).

Equations

• EulerLpPointwiseMultiplier.operator μ A hA C hC = (EulerLpPointwiseMultiplier.linear μ A hA C hC).mkContinuous C ⋯

theorem EulerLpPointwiseMultiplier.operator_ae {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) (u : ↥(MeasureTheory.Lp E 2 μ)) : ↑↑((operator μ A hA C hC) u) =ᵐ[μ] fun (x : X) => (A x) (↑↑u x)

theorem EulerLpPointwiseMultiplier.operator_bound {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (A : X → E →L[ℝ] F) (hA : MeasureTheory.AEStronglyMeasurable A μ) (C : ℝ) (hC : ∀ (x : X), ‖A x‖ ≤ C) (u : ↥(MeasureTheory.Lp E 2 μ)) : ‖(operator μ A hA C hC) u‖ ≤ C * ‖u‖

theorem EulerLpPointwiseMultiplier.operator_strongly_continuous {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (C : ℝ) {K : Type u_4} [TopologicalSpace K] [FirstCountableTopology K] (B : K → X → E →L[ℝ] F) (hB : ∀ (t : K), MeasureTheory.AEStronglyMeasurable (B t) μ) (hBt : ∀ (x : X), Continuous fun (t : K) => B t x) (hBC : ∀ (t : K) (x : X), ‖B t x‖ ≤ C) (u : ↥(MeasureTheory.Lp E 2 μ)) : Continuous fun (t : K) => (operator μ (B t) ⋯ C ⋯) u

theorem EulerLpPointwiseMultiplier.operator_path_continuous {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure X) (C : ℝ) {K : Type u_4} [TopologicalSpace K] [FirstCountableTopology K] (B : K → X → E →L[ℝ] F) (hB : ∀ (t : K), MeasureTheory.AEStronglyMeasurable (B t) μ) (hBt : ∀ (x : X), Continuous fun (t : K) => B t x) (hBC : ∀ (t : K) (x : X), ‖B t x‖ ≤ C) (u : K → ↥(MeasureTheory.Lp E 2 μ)) (hu : Continuous u) : Continuous fun (t : K) => (operator μ (B t) ⋯ C ⋯) (u t)

@[reducible, inline]

abbrev EulerVolumeSobolevPath.Tensor (n : ℕ) : Type

Tensor: an abbreviation for Vector3 [×n]→L[ℝ] Vector3.

Equations

• EulerVolumeSobolevPath.Tensor n = (EulerLiftedGradientSpace.Vector3 [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3)

@[instance_reducible]

noncomputable def EulerVolumeSobolevPath.instVolumeSobolevPath1 (n : ℕ) : NormedAddCommGroup (Tensor n)

Cache the standard NormedAddCommGroup (Tensor n) instance to shorten typeclass synthesis.

Equations

• EulerVolumeSobolevPath.instVolumeSobolevPath1 n = inferInstance

@[instance_reducible]

noncomputable def EulerVolumeSobolevPath.instVolumeSobolevPath2 (n : ℕ) : NormedSpace ℝ (Tensor n)

Cache the standard NormedSpace ℝ (Tensor n) instance to shorten typeclass synthesis.

Equations

• EulerVolumeSobolevPath.instVolumeSobolevPath2 n = inferInstance

@[instance_reducible]

noncomputable def EulerVolumeSobolevPath.instVolumeSobolevPath3 (a b : ℕ) : NormedAddCommGroup (Tensor a →L[ℝ] Tensor b)

Cache the standard NormedAddCommGroup (Tensor a →L[ℝ] Tensor b) instance to shorten typeclass synthesis.

Equations

• EulerVolumeSobolevPath.instVolumeSobolevPath3 a b = inferInstance

@[instance_reducible]

noncomputable def EulerVolumeSobolevPath.instVolumeSobolevPath4 (a b : ℕ) : NormedSpace ℝ (Tensor a →L[ℝ] Tensor b)

Cache the standard NormedSpace ℝ (Tensor a →L[ℝ] Tensor b) instance to shorten typeclass synthesis.

Equations

• EulerVolumeSobolevPath.instVolumeSobolevPath4 a b = inferInstance

theorem EulerVolumeSobolevPath.instVolumeSobolevPath5 (a b : ℕ) : SecondCountableTopologyEither EulerLiftedGradientSpace.Vector3 (Tensor a →L[ℝ] Tensor b)

noncomputable def EulerVolumeSobolevPath.pulledJetPath {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : K), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (u : (i : ℕ) → C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))) (i : ℕ) : C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))

Pulled jet path, bundling toFun, continuous_toFun.

Equations

• EulerVolumeSobolevPath.pulledJetPath Y hmp u i = { toFun := fun (t : K) => (MeasureTheory.Lp.compMeasurePreserving ⇑(Y t) ⋯) ((u i) t), continuous_toFun := ⋯ }

theorem EulerVolumeSobolevPath.pulledJetPath_ae {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : K), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (u : (i : ℕ) → C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))) (g : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hu : ∀ (i : ℕ) (t : K), ↑↑((u i) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ i (g t)) (i : ℕ) (t : K) : ↑↑((pulledJetPath Y hmp u i) t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (g t) ((Y t) x)

noncomputable def EulerVolumeSobolevPath.partitionCoefficient {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) {n : ℕ} (c : OrderedFinpartition n) (t : K) (x : EulerLiftedGradientSpace.Vector3) : Tensor c.length →L[ℝ] Tensor n

Partition coefficient, given by (c.compAlongOrderedFinpartitionL ℝ Vector3 Vector3 Vector3).flipMultilinear (fun i => iteratedFDeriv ℝ (c.partSize i) (Y t) x).

Equations

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

theorem EulerVolumeSobolevPath.partitionCoefficient_apply {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) {n : ℕ} (c : OrderedFinpartition n) (t : K) (x : EulerLiftedGradientSpace.Vector3) (v : Tensor c.length) : (partitionCoefficient Y c t x) v = c.compAlongOrderedFinpartition v fun (i : Fin c.length) => iteratedFDeriv ℝ (c.partSize i) (⇑(Y t)) x

def EulerVolumeSobolevPath.partitionBound {n : ℕ} (D : ℝ) (c : OrderedFinpartition n) : ℝ

Partition bound, given by ∏ i : Fin c.length, D^(c.partSize i).

Equations

• EulerVolumeSobolevPath.partitionBound D c = ∏ i : Fin c.length, D ^ c.partSize i

theorem EulerVolumeSobolevPath.partitionCoefficient_continuous {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) {n : ℕ} (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : K × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (c : OrderedFinpartition n) : Continuous (Function.uncurry (partitionCoefficient Y c))

theorem EulerVolumeSobolevPath.partitionCoefficient_aestronglyMeasurable {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) {n : ℕ} (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : K × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (c : OrderedFinpartition n) (t : K) : MeasureTheory.AEStronglyMeasurable (partitionCoefficient Y c t) MeasureTheory.volume

theorem EulerVolumeSobolevPath.partitionCoefficient_bound {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) {n : ℕ} (D : ℝ) (hD : 0 ≤ D) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) (c : OrderedFinpartition n) (t : K) (x : EulerLiftedGradientSpace.Vector3) : ‖partitionCoefficient Y c t x‖ ≤ partitionBound D c

noncomputable def EulerVolumeSobolevPath.partitionPath {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : K), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (u : (i : ℕ) → C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))) {n : ℕ} (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : K × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) [FirstCountableTopology K] (c : OrderedFinpartition n) : C(K, ↥(MeasureTheory.Lp (Tensor n) 2 MeasureTheory.volume))

Partition path, bundling toFun, continuous_toFun.

Equations

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

theorem EulerVolumeSobolevPath.partitionPath_ae {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : K), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (u : (i : ℕ) → C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))) {n : ℕ} (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : K × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) [FirstCountableTopology K] (g : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hu : ∀ (i : ℕ) (t : K), ↑↑((u i) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ i (g t)) (c : OrderedFinpartition n) (t : K) : ↑↑((partitionPath Y hmp u D hD hJ hB c) t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => c.compAlongOrderedFinpartition (iteratedFDeriv ℝ c.length (g t) ((Y t) x)) fun (i : Fin c.length) => iteratedFDeriv ℝ (c.partSize i) (⇑(Y t)) x

noncomputable def EulerVolumeSobolevPath.tensorPath {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : K), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (u : (i : ℕ) → C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))) {n : ℕ} (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : K × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) [FirstCountableTopology K] : C(K, ↥(MeasureTheory.Lp (Tensor n) 2 MeasureTheory.volume))

Tensor path, given by ∑ c : OrderedFinpartition n, partitionPath Y hmp u D hD hJ hB c.

Equations

• EulerVolumeSobolevPath.tensorPath Y hmp u D hD hJ hB = ∑ c : OrderedFinpartition n, EulerVolumeSobolevPath.partitionPath Y hmp u D hD hJ hB c

theorem EulerVolumeSobolevPath.tensorPath_ae {K : Type u_1} [TopologicalSpace K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : K), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (u : (i : ℕ) → C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))) {n : ℕ} (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : K × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) [FirstCountableTopology K] (g : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hg : ∀ (t : K), ContDiff ℝ (↑⊤) (g t)) (hY : ∀ (t : K), ContDiff ℝ ↑⊤ ⇑(Y t)) (hu : ∀ (i : ℕ) (t : K), ↑↑((u i) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ i (g t)) (t : K) : ↑↑((tensorPath Y hmp u D hD hJ hB) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (g t ∘ ⇑(Y t))

Actual all-order field towers retain their spatial Sobolev regularity after a smooth volume-preserving change of coordinates.

Actual Sobolev integrability under a smooth volume-preserving change of variables, with an explicit finite-order composition constant.

theorem EulerVolumeSobolevComposition.compositionTensor_pointwise (f g : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (D : ℝ) (hjet : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i f x‖ ≤ D ^ i) (x : EulerLiftedGradientSpace.Vector3) : ‖iteratedFDeriv ℝ n (g ∘ f) x‖ ≤ ↑n.factorial * D ^ n * ∑ i : Fin (n + 1), ‖iteratedFDeriv ℝ (↑i) g (f x)‖

theorem EulerVolumeSobolevComposition.composedJetNorm_memLp (f g : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (n : ℕ) (hmp : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (hLp : ∀ i ≤ n, MeasureTheory.MemLp (iteratedFDeriv ℝ i g) 2 MeasureTheory.volume) (i : Fin (n + 1)) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.Vector3) => ‖iteratedFDeriv ℝ (↑i) g (f x)‖) 2 MeasureTheory.volume

theorem EulerVolumeSobolevComposition.compositionTensor_memLp (f g : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (D : ℝ) (hD : 0 ≤ D) (hjet : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i f x‖ ≤ D ^ i) (hmp : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (hLp : ∀ i ≤ n, MeasureTheory.MemLp (iteratedFDeriv ℝ i g) 2 MeasureTheory.volume) : MeasureTheory.MemLp (iteratedFDeriv ℝ n (g ∘ f)) 2 MeasureTheory.volume

noncomputable def EulerVolumeSobolevComposition.compositionTensorLp (f g : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (D : ℝ) (hD : 0 ≤ D) (hjet : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i f x‖ ≤ D ^ i) (hmp : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (hLp : ∀ i ≤ n, MeasureTheory.MemLp (iteratedFDeriv ℝ i g) 2 MeasureTheory.volume) : ↥(MeasureTheory.Lp (EulerLiftedGradientSpace.Vector3 [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3) 2 MeasureTheory.volume)

Composition tensor Lᵖ, given by (compositionTensor_memLp f g hf hg n D hD hjet hmp hLp).toLp (iteratedFDeriv ℝ n (g ∘ f)).

Equations

• EulerVolumeSobolevComposition.compositionTensorLp f g hf hg n D hD hjet hmp hLp = MeasureTheory.MemLp.toLp (iteratedFDeriv ℝ n (g ∘ f)) ⋯

theorem EulerVolumeSobolevComposition.compositionTensorLp_norm_le (f g : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (D : ℝ) (hD : 0 ≤ D) (hjet : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i f x‖ ≤ D ^ i) (hmp : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) (hLp : ∀ i ≤ n, MeasureTheory.MemLp (iteratedFDeriv ℝ i g) 2 MeasureTheory.volume) : ‖compositionTensorLp f g hf hg n D hD hjet hmp hLp‖ ≤ ↑n.factorial * D ^ n * ∑ i : Fin (n + 1), (MeasureTheory.eLpNorm (iteratedFDeriv ℝ (↑i) g) 2 MeasureTheory.volume).toReal

theorem EulerVolumeSobolevPath.tensorPath_norm_le {K : Type u_1} [TopologicalSpace K] [FirstCountableTopology K] (Y : C(K, C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : K), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (u : (i : ℕ) → C(K, ↥(MeasureTheory.Lp (Tensor i) 2 MeasureTheory.volume))) {n : ℕ} (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : K × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : K) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) (g : K → EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3) (hg : ∀ (t : K), ContDiff ℝ (↑⊤) (g t)) (hY : ∀ (t : K), ContDiff ℝ ↑⊤ ⇑(Y t)) (hu : ∀ (i : ℕ) (t : K), ↑↑((u i) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ i (g t)) (t : K) : ‖(tensorPath Y hmp u D hD hJ hB) t‖ ≤ ↑n.factorial * D ^ n * ∑ i : Fin (n + 1), ‖(u ↑i) t‖

noncomputable def EulerAllOrderCorrectionData.FieldTower.volumePointField {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y : C(↑(Set.Icc 0 T), C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (t : ↑(Set.Icc 0 T)) : EulerLiftedGradientSpace.Vector3 → EulerLiftedGradientSpace.Vector3

Volume point field, given by A.physicalPointField k m t ∘ Y t.

Equations

• A.volumePointField k m Y t = A.physicalPointField k m t ∘ ⇑(Y t)

noncomputable def EulerAllOrderCorrectionData.FieldTower.volumeTensorPath {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y : C(↑(Set.Icc 0 T), C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : ↑(Set.Icc 0 T)), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (n : ℕ) (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : ↑(Set.Icc 0 T) × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp (EulerLiftedGradientSpace.Vector3 [×n]→L[ℝ] EulerLiftedGradientSpace.Vector3) 2 MeasureTheory.volume))

Volume tensor path, given by EulerVolumeSobolevPath.tensorPath Y hmp (fun i => A.physicalTensorPath k m i) D hD hJ hB.

Equations

• A.volumeTensorPath k m Y hmp n D hD hJ hB = EulerVolumeSobolevPath.tensorPath Y hmp (fun (i : ℕ) => A.physicalTensorPath k m i) D hD hJ hB

theorem EulerAllOrderCorrectionData.FieldTower.volumePointField_smooth {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y : C(↑(Set.Icc 0 T), C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hY : ∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ ↑⊤ ⇑(Y t)) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (A.volumePointField k m Y t)

theorem EulerAllOrderCorrectionData.FieldTower.volumeTensorPath_ae {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y : C(↑(Set.Icc 0 T), C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : ↑(Set.Icc 0 T)), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (n : ℕ) (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : ↑(Set.Icc 0 T) × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) (hY : ∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ ↑⊤ ⇑(Y t)) (t : ↑(Set.Icc 0 T)) : ↑↑((A.volumeTensorPath k m Y hmp n D hD hJ hB) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n (A.volumePointField k m Y t)

theorem EulerAllOrderCorrectionData.FieldTower.volumeTensorPath_norm_le {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Y : C(↑(Set.Icc 0 T), C(EulerLiftedGradientSpace.Vector3, EulerLiftedGradientSpace.Vector3))) (hmp : ∀ (t : ↑(Set.Icc 0 T)), MeasureTheory.MeasurePreserving (⇑(Y t)) MeasureTheory.volume MeasureTheory.volume) (n : ℕ) (D : ℝ) (hD : 0 ≤ D) (hJ : ∀ (i : ℕ), 1 ≤ i → i ≤ n → Continuous fun (z : ↑(Set.Icc 0 T) × EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ i (⇑(Y z.1)) z.2) (hB : ∀ (i : ℕ), 1 ≤ i → i ≤ n → ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3), ‖iteratedFDeriv ℝ i (⇑(Y t)) x‖ ≤ D ^ i) (hY : ∀ (t : ↑(Set.Icc 0 T)), ContDiff ℝ ↑⊤ ⇑(Y t)) (t : ↑(Set.Icc 0 T)) : ‖(A.volumeTensorPath k m Y hmp n D hD hJ hB) t‖ ≤ ↑n.factorial * D ^ n * ∑ i : Fin (n + 1), EulerCylinderPhysicalTensor.frequencyFactor k m ^ ↑i * 4 ^ ↑i * √(2 / P + 2 * P) * ‖(A.realization (↑i + 1)) t‖

A finite-order Sobolev composition constant obtained from the actual parent deformation. No inverse-flow derivative budget is assumed.

def EulerPacketInverseFlowGevrey.finiteOrderConstant (C R : ℝ) (n : ℕ) : ℝ

Finite order constant, given by 1+9*C^2*(sourceInverseRadius C R)^n*(n.factorial : ℝ)^2.

Equations

• EulerPacketInverseFlowGevrey.finiteOrderConstant C R n = 1 + 9 * C ^ 2 * EulerPacketInverseFlowGevrey.sourceInverseRadius C R ^ n * ↑n.factorial ^ 2

theorem EulerPacketInverseFlowGevrey.sourceInverseRadius_one_le (C R : ℝ) (hR : 0 ≤ R) : 1 ≤ sourceInverseRadius C R

theorem EulerPacketInverseFlowGevrey.finiteOrderConstant_one_le (C R : ℝ) (hR : 0 ≤ R) (n : ℕ) : 1 ≤ finiteOrderConstant C R n

theorem EulerPacketInverseFlowGevrey.inverseFlow_finiteOrderBound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n i : ℕ) (hi : 1 ≤ i) (hin : i ≤ n) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ i (Y t) x‖ ≤ finiteOrderConstant C R n ^ i

theorem EulerPacketSourceVolumeSobolev.inversePath_volume {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (t : ↑(Set.Icc 0 D.T)) : MeasureTheory.MeasurePreserving (⇑((EulerFlowL2Transport.inversePath Y hYjoint) t)) MeasureTheory.volume MeasureTheory.volume

noncomputable def EulerPacketSourceVolumeSobolev.tensorPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) : C(↑(Set.Icc 0 D.T), ↥(MeasureTheory.Lp (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space) 2 MeasureTheory.volume))

Tensor path, constructed using Z.volumeTensorPath.

Equations

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

theorem EulerPacketSourceVolumeSobolev.tensorPath_ae {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) : ↑↑((tensorPath D Z k m X Y hX hYX hXY hYjoint R C hR hC hdet hF n) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n fun (x : EulerSmoothLimit.Space) => Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k m (Y t x))

theorem EulerPacketSourceVolumeSobolev.tensorPath_norm_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) : ‖(tensorPath D Z k m X Y hX hYX hXY hYjoint R C hR hC hdet hF n) t‖ ≤ ↑n.factorial * EulerPacketInverseFlowGevrey.finiteOrderConstant C R n ^ n * ∑ i : Fin (n + 1), EulerCylinderPhysicalTensor.frequencyFactor k m ^ ↑i * 4 ^ ↑i * √(2 / P + 2 * P) * ‖(Z.realization (↑i + 1)) t‖

Actual Eulerian reconstructions have every spatial derivative in L², continuously in time. Sobolev embedding also supplies bounded smooth coefficient paths for the velocity and pressure force.

Reconstruction W=κFz is a genuine all-order field tower. Its graph restriction and its actual inverse-flow pullback are continuous spatial L² paths, with no independent integrability assumption on the perturbation.

noncomputable def EulerPacketPhysicalField.reconstructedTower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) : EulerAllOrderCorrectionData.FieldTower P D.T

Reconstructed tower, given by (Z.multiply ((frameCoefficient D).toCoefficientTower P)).smul κ.

Equations

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

theorem EulerPacketPhysicalField.reconstructedTower_pointField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : (reconstructedTower D P κ Z).pointField t x = κ • ((D.F.field t) x.1) (Z.pointField t x)

noncomputable def EulerPacketPhysicalField.graphPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) : C(↑(Set.Icc 0 D.T), ↥(MeasureTheory.Lp EulerSmoothLimit.Space 2 MeasureTheory.volume))

Graph path, given by (reconstructedTower D P κ Z).canonicalGraphWordPath (physicalPhase P k D.m₀) (physicalPhase_continuous P k D.m₀) 0 Fin.elim0.

Equations

• EulerPacketPhysicalField.graphPath D P κ Z k = (EulerPacketPhysicalField.reconstructedTower D P κ Z).canonicalGraphWordPath (EulerCylinderPhysicalTensor.physicalPhase P k D.m₀) ⋯ 0 Fin.elim0

theorem EulerPacketPhysicalField.graphPath_ae {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (t : ↑(Set.Icc 0 D.T)) : ↑↑((graphPath D P κ Z k) t) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => κ • ((D.F.field t) x) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ x))

noncomputable def EulerPacketPhysicalField.graphTensorPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (n : ℕ) : C(↑(Set.Icc 0 D.T), ↥(MeasureTheory.Lp (EulerSmoothLimit.Space [×n]→L[ℝ] EulerSmoothLimit.Space) 2 MeasureTheory.volume))

Graph tensor path, given by (reconstructedTower D P κ Z).physicalTensorPath k D.m₀ n.

Equations

• EulerPacketPhysicalField.graphTensorPath D P κ Z k n = (EulerPacketPhysicalField.reconstructedTower D P κ Z).physicalTensorPath k D.m₀ n

theorem EulerPacketPhysicalField.graphTensorPath_ae {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) : ↑↑((graphTensorPath D P κ Z k n) t) =ᵐ[MeasureTheory.volume] iteratedFDeriv ℝ n fun (x : EulerSmoothLimit.Space) => κ • ((D.F.field t) x) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ x))

noncomputable def EulerPacketPhysicalField.eulerianPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ((D.F.field t) x).det = 1) (k : ℝ) : C(↑(Set.Icc 0 D.T), ↥(MeasureTheory.Lp EulerSmoothLimit.Space 2 MeasureTheory.volume))

Eulerian path, given by transportPath X Y (fun t x => D.F.field t x) hX hYX hXY hY hdet (graphPath D P κ Z k).

Equations

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

theorem EulerPacketPhysicalField.eulerianPath_ae {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ((D.F.field t) x).det = 1) (k : ℝ) (t : ↑(Set.Icc 0 D.T)) : ↑↑((eulerianPath D P κ Z X Y hX hYX hXY hY hdet k) t) =ᵐ[MeasureTheory.volume] fun (x : EulerSmoothLimit.Space) => κ • ((D.F.field t) (Y t x)) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y t x)))

theorem EulerPacketPhysicalField.eulerianPath_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ((D.F.field t) x).det = 1) (k : ℝ) (t : ↑(Set.Icc 0 D.T)) : ‖(eulerianPath D P κ Z X Y hX hYX hXY hY hdet k) t‖ = ‖(graphPath D P κ Z k) t‖

The actual source-flow pullback is a smooth spatial L² field at every time. Its tensor paths also give a bounded smooth coefficient path, with continuity in the uniform norm at every spatial order.

noncomputable def EulerPacketSourceVolumeSobolev.smoothField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Smooth field, bundling field, smooth, integrable.

Equations

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

theorem EulerPacketSourceVolumeSobolev.smoothField_jetLp {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) : (smoothField D Z k m X Y hX hYX hXY hYjoint R C hR hC hdet hF t).jetLp n = (tensorPath D Z k m X Y hX hYX hXY hYjoint R C hR hC hdet hF n) t

theorem EulerPacketSourceVolumeSobolev.smoothField_jetLp_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 D.T)) => (smoothField D Z k m X Y hX hYX hXY hYjoint R C hR hC hdet hF t).jetLp n

noncomputable def EulerPacketSourceVolumeSobolev.smoothCoefficientPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) EulerSmoothLimit.Space

Smooth coefficient path, constructed using EulerMeanSobolevBoundedField.coefficientPath.

Equations

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

theorem EulerPacketSourceVolumeSobolev.smoothCoefficientPath_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) {P : ℝ} [Fact (0 < P)] (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (m : EulerSmoothLimit.Space) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hYjoint : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ((smoothCoefficientPath D Z k m X Y hX hYX hXY hYjoint R C hR hC hdet hF).field t) x = Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k m (Y t x))

noncomputable def EulerPacketPhysicalField.pressureForceTower {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) : EulerAllOrderCorrectionData.FieldTower P D.T

Pressure force tower, given by (Z.multiply ((inverseCoefficient D).adjoint.toCoefficientTower P)).smul κ.

Equations

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

theorem EulerPacketPhysicalField.pressureForceTower_pointField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (t : ↑(Set.Icc 0 D.T)) (x : EulerLiftedGradientSpace.LiftDomain P) : (pressureForceTower D P κ Z).pointField t x = κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) x.1)) (Z.pointField t x)

noncomputable def EulerPacketPhysicalField.eulerianSmoothField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Eulerian smooth field, given by EulerPacketSourceVolumeSobolev.smoothField D (reconstructedTower D P κ Z) k D.m₀ X Y hX hYX hXY hY R C hR hC hdet hF t.

Equations

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

theorem EulerPacketPhysicalField.eulerianSmoothField_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (eulerianSmoothField D P κ Z k X Y hX hYX hXY hY R C hR hC hdet hF t).field x = κ • ((D.F.field t) (Y t x)) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y t x)))

theorem EulerPacketPhysicalField.eulerianSmoothField_jetLp_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 D.T)) => (eulerianSmoothField D P κ Z k X Y hX hYX hXY hY R C hR hC hdet hF t).jetLp n

noncomputable def EulerPacketPhysicalField.eulerianCoefficientPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) EulerSmoothLimit.Space

Eulerian coefficient path, given by EulerPacketSourceVolumeSobolev.smoothCoefficientPath D (reconstructedTower D P κ Z) k D.m₀ X Y hX hYX hXY hY R C hR hC hdet hF.

Equations

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

theorem EulerPacketPhysicalField.eulerianCoefficientPath_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ((eulerianCoefficientPath D P κ Z k X Y hX hYX hXY hY R C hR hC hdet hF).field t) x = κ • ((D.F.field t) (Y t x)) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y t x)))

noncomputable def EulerPacketPhysicalField.pressureForceSmoothField {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Pressure force smooth field, given by EulerPacketSourceVolumeSobolev.smoothField D (pressureForceTower D P κ Z) k D.m₀ X Y hX hYX hXY hY R C hR hC hdet hF t.

Equations

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

theorem EulerPacketPhysicalField.pressureForceSmoothField_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (pressureForceSmoothField D P κ Z k X Y hX hYX hXY hY R C hR hC hdet hF t).field x = κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y t x))) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y t x)))

theorem EulerPacketPhysicalField.pressureForceSmoothField_jetLp_continuous {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 D.T)) => (pressureForceSmoothField D P κ Z k X Y hX hYX hXY hY R C hR hC hdet hF t).jetLp n

noncomputable def EulerPacketPhysicalField.pressureForceCoefficientPath {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 D.T)) EulerSmoothLimit.Space

Pressure force coefficient path, given by EulerPacketSourceVolumeSobolev.smoothCoefficientPath D (pressureForceTower D P κ Z) k D.m₀ X Y hX hYX hXY hY R C hR hC hdet hF.

Equations

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

theorem EulerPacketPhysicalField.pressureForceCoefficientPath_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P D.T) (k : ℝ) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hYX : ∀ (t : ↑(Set.Icc 0 D.T)), Function.LeftInverse (Y t) (X t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)), Function.RightInverse (Y t) (X t)) (hY : Continuous (Function.uncurry Y)) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ((pressureForceCoefficientPath D P κ Z k X Y hX hYX hXY hY R C hR hC hdet hF).field t) x = κ • (ContinuousLinearMap.adjoint ((D.FInv.field t) (Y t x))) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k D.m₀ (Y t x)))

Actual odd parent fields supply the parity data for both initialized packet branches. The resulting corrected coefficient, and hence the actual next particle map, retain oddness without a new symmetry premise.

The actual corrected lifted velocity is odd when its prescribed correction data have the checked parity. Passing from L² symmetry to the canonical point field supplies symmetry of the real flow coefficient.

theorem EulerAllOrderCorrectionData.FieldTower.pointField_odd {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (ho : ∀ (t : ↑(Set.Icc 0 T)), -(EulerCylinderReflection.reflection P) (A.field t) = A.field t) (t : ↑(Set.Icc 0 T)) : Function.Odd (A.pointField t)

theorem EulerAllOrderDriftCorrection.Budget.correctedFieldTower_odd (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) (E : EulerCorrectionAssembly.ParityData P A) (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection P) ((correctedFieldTower P B).field t) = (correctedFieldTower P B).field t

theorem EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient_odd (P : ℝ) [Fact (0 < P)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data P T} (B : Budget P hT A) {raw : EulerPacketProfileRecursion.VectorField} (G : EulerPacketCylinderField.Field P T raw) (hG : A.approximation = G.toFieldTower) (E : EulerCorrectionAssembly.ParityData P A) (t : ↑(Set.Icc 0 T)) : Function.Odd ⇑((liftedPacketCoefficient P B G).field t)

theorem EulerParentPacketFrames.OddData.forwardCorrectionParity {A : Parent} (O : OddData A) (H : LowBounds A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S) (α : ℝ) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) : EulerCorrectionAssembly.ParityData EulerPacketTerminalDatum.period (EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm R S hS) ⋯ δ hδ ξ hs α ⋯ N hN k hk)

theorem EulerParentPacketFrames.OddData.joinedCorrectionParity {A : Parent} (O : OddData A) (H : LowBounds A) {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S) (α τ : ℝ) (hτ : 0 < τ) (hτT : τ < A.T) (N : ℕ) (hN : 1 ≤ N) (k : ℝ) (hk : 4 ≤ k) : EulerCorrectionAssembly.ParityData EulerPacketTerminalDatum.period (EulerPacketTerminalDatum.initializedCorrectionData (A.meanData H) (A.transverseData m hm R S hS) ⋯ τ hτ hτT (A.historyOn H m hm R S hS τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk)

theorem EulerParentPacketFrames.OddData.childOfPacket {A : Parent} (O : OddData A) {P : ℝ} [Fact (0 < P)] {C : EulerAllOrderCorrectionData.Data P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ C) (E : EulerCorrectionAssembly.ParityData P C) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : C.approximation = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k C.direction) ((G.A.field t) z) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : OddData (A.child G k C.direction hgraph nextEll hnext hnext1)

Actual physical L² fields of a packet over a parent. The genuine inverse and the proved parent label bound supply all reconstruction regularity, and the physical spatial scale is retained exactly.

theorem EulerParentPacketFrames.ParticleInverse.normalized_scaled {A : Parent} (I : ParticleInverse A) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : I.normalized t (A.ell⁻¹ • x) = A.ell⁻¹ • I.field t x

noncomputable def EulerParentPacketFrames.LabelData.packetVelocityField {A : Parent} (L : LabelData A) (I : ParticleInverse A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P A.T) (k : ℝ) (t : ↑(Set.Icc 0 A.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Packet velocity field, constructed using scaleField.

Equations

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

noncomputable def EulerParentPacketFrames.LabelData.packetForceField {A : Parent} (L : LabelData A) (I : ParticleInverse A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P A.T) (k : ℝ) (t : ↑(Set.Icc 0 A.T)) : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

Packet force field, constructed using scaleField.

Equations

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

theorem EulerParentPacketFrames.LabelData.packetVelocityField_apply {A : Parent} (L : LabelData A) (I : ParticleInverse A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P A.T) (k : ℝ) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (L.packetVelocityField I m hm J support hSupport P κ Z k t).field x = A.ell • κ • ((A.frame.field t) (A.ell⁻¹ • I.field t x)) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k m (A.ell⁻¹ • I.field t x)))

theorem EulerParentPacketFrames.LabelData.packetForceField_apply {A : Parent} (L : LabelData A) (I : ParticleInverse A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P A.T) (k : ℝ) (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space) : (L.packetForceField I m hm J support hSupport P κ Z k t).field x = A.ell • κ • (ContinuousLinearMap.adjoint ((A.inverse.field t) (A.ell⁻¹ • I.field t x))) (Z.pointField t (EulerGraphPressurePotential.cylinderGraph P k m (A.ell⁻¹ • I.field t x)))

theorem EulerParentPacketFrames.LabelData.packetVelocityField_continuous {A : Parent} (L : LabelData A) (I : ParticleInverse A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P A.T) (k : ℝ) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 A.T)) => (L.packetVelocityField I m hm J support hSupport P κ Z k t).jetLp n

theorem EulerParentPacketFrames.LabelData.packetForceField_continuous {A : Parent} (L : LabelData A) (I : ParticleInverse A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) (P : ℝ) [Fact (0 < P)] (κ : ℝ) (Z : EulerAllOrderCorrectionData.FieldTower P A.T) (k : ℝ) (n : ℕ) : Continuous fun (t : ↑(Set.Icc 0 A.T)) => (L.packetForceField I m hm J support hSupport P κ Z k t).jetLp n

The constructed child Euler evolution remains in the actual all-order spatial Sobolev class. Its fields are the parent fields plus the very same exact packet used in the particle-map construction.

noncomputable def EulerParentPacketFrames.SobolevData.child {A : Parent} {E : Evolution A} (F : SobolevData E) (L : LabelData A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : SobolevData (E.child m hm J support hSupport B residual V hV G hG k hk hgraph nextEll hnext hnext1)

Child, bundling velocity, force, velocity_match, force_match and the required compatibility proofs.

Equations

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

structure EulerParentPacketFrames.SmoothState (A : Parent) : Type

Smooth state data, collecting evolution, regularity, labels, odd.

• evolution : Evolution A

  Evolution of SmoothState, of type Evolution A.

• regularity : SobolevData self.evolution

  Regularity of SmoothState, of type SobolevData evolution.

• labels : LabelData A

  Label type of SmoothState, of type LabelData A.

• odd : OddData A

def EulerParentPacketFrames.SmoothState.restrictTime {A : Parent} (S : SmoothState A) (T : ℝ) (hT : 0 < T) (hTA : T ≤ A.T) : SmoothState (A.restrictTime T hT hTA)

Restrict time, bundling evolution, regularity, labels, odd.

Equations

• S.restrictTime T hT hTA = { evolution := S.evolution.restrictTime T hT hTA, regularity := S.regularity.restrictTime T hT hTA, labels := S.labels.restrictTime T hT hTA, odd := ⋯ }

noncomputable def EulerParentPacketFrames.SmoothState.packetChild {A : Parent} (S : SmoothState A) {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (support : Set EulerSmoothLimit.Space) (hSupport : IsCompact support) {P : ℝ} [Fact (0 < P)] {κ : ℝ} {hκ : |κ| ≤ 1} {Z R : EulerAllOrderCorrectionData.FieldTower P A.T} (B : EulerAllOrderDriftCorrection.Budget P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (residual : EulerAllOrderDriftCorrection.ApproximationResidual P ⋯ (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) {raw : EulerPacketProfileRecursion.VectorField} (V : EulerPacketCylinderField.Field P A.T raw) (hV : Z = V.toFieldTower) (symmetry : EulerCorrectionAssembly.ParityData P (EulerPacketCorrectionCoefficients.correctionData (A.transverseData m hm J support hSupport) P κ hκ Z R)) (G : EulerPhysicalGraphFlowBounds.Data P A.T) (hG : G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient P B V) (k : ℝ) (hk : k * κ = 1) (hgraph : ∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (labels : LabelData (A.child G k m hgraph nextEll hnext hnext1)) : SmoothState (A.child G k m hgraph nextEll hnext hnext1)

Packet child, bundling evolution, regularity, labels, odd.

Equations

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