The actual physical graph flow has smooth square-integrable displacement, velocity and acceleration, with explicit Gevrey bounds. Every input estimate is on the original lifted velocity or its genuine time derivative; no regularity of the output flow is assumed.

The true physical graph flow and its first two time derivatives. The change of labels is an actual ODE conjugacy, and the resulting three-dimensional flow preserves ordinary Lebesgue volume.

The graph restriction of the actual lifted flow is the actual flow of a smooth three-dimensional velocity. It preserves ordinary spatial volume when the original lifted velocity has zero trace.

A lifted flow tangent to the oscillating graph gives an actual three-dimensional flow, with inverse and the projected differential equation. Graph invariance follows from a conserved linear functional.

noncomputable def EulerGraphInvariantFlow.graphLinear (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3 →L[ℝ] EulerLiftedGradientSpace.LiftTangent

Graph linear, given by (ContinuousLinearMap.id ℝ Vector3).prod (k • toDual ℝ Vector3 m).

Equations

• EulerGraphInvariantFlow.graphLinear k m = (ContinuousLinearMap.id ℝ EulerLiftedGradientSpace.Vector3).prod (k • (InnerProductSpace.toDual ℝ EulerLiftedGradientSpace.Vector3) m)

@[simp]

theorem EulerGraphInvariantFlow.graphLinear_apply (k : ℝ) (m x : EulerLiftedGradientSpace.Vector3) : (graphLinear k m) x = (x, k * inner ℝ m x)

noncomputable def EulerGraphInvariantFlow.graphConstraint (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.LiftTangent →L[ℝ] ℝ

Graph constraint, given by snd ℝ Vector3 ℝ - k • (toDual ℝ Vector3 m).comp (fst ℝ Vector3 ℝ).

Equations

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

@[simp]

theorem EulerGraphInvariantFlow.graphConstraint_apply (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (z : EulerLiftedGradientSpace.LiftTangent) : (graphConstraint k m) z = z.2 - k * inner ℝ m z.1

theorem EulerGraphInvariantFlow.graphConstraint_graph (k : ℝ) (m x : EulerLiftedGradientSpace.Vector3) : (graphConstraint k m) ((graphLinear k m) x) = 0

theorem EulerGraphInvariantFlow.graphConstraint_transport (k κ : ℝ) (hk : k * κ = 1) (m v : EulerLiftedGradientSpace.Vector3) : (graphConstraint k m) (EulerMetricTransport.transportDirection κ m v) = 0

theorem EulerGraphInvariantFlow.graphConstraint_flow (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) (V.velocity t z) = 0) (s t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : (graphConstraint k m) (V.flow s t z) = (graphConstraint k m) z

noncomputable def EulerGraphInvariantFlow.graphFlow (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (s t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3

Graph flow, given by (V.flow s t (graphLinear k m x)).1.

Equations

• EulerGraphInvariantFlow.graphFlow k m V s t x = (V.flow s t ((EulerGraphInvariantFlow.graphLinear k m) x)).1

theorem EulerGraphInvariantFlow.graphFlow_invariant (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) (V.velocity t z) = 0) (s t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : V.flow s t ((graphLinear k m) x) = (graphLinear k m) (graphFlow k m V s t x)

@[simp]

theorem EulerGraphInvariantFlow.graphFlow_initial (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (s : ℝ) (x : EulerLiftedGradientSpace.Vector3) : graphFlow k m V s s x = x

theorem EulerGraphInvariantFlow.graphFlow_inverse (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) (V.velocity t z) = 0) (s t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : graphFlow k m V t s (graphFlow k m V s t x) = x

theorem EulerGraphInvariantFlow.graphFlow_hasDerivAt (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) (V.velocity t z) = 0) (s t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : HasDerivAt (fun (r : ℝ) => graphFlow k m V s r x) (V.velocity t ((graphLinear k m) (graphFlow k m V s t x))).1 t

theorem EulerGraphInvariantFlow.graphFlow_continuous (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (s t : ℝ) : Continuous (graphFlow k m V s t)

theorem EulerGraphInvariantFlow.graphFlow_forward_joint_continuous (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) : Continuous fun (r : ℝ × EulerLiftedGradientSpace.Vector3) => graphFlow k m V 0 r.1 r.2

theorem EulerGraphInvariantFlow.graphFlow_backward_joint_continuous (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) : Continuous fun (r : ℝ × EulerLiftedGradientSpace.Vector3) => graphFlow k m V r.1 0 r.2

A graph-tangent lifted velocity has the same ordinary divergence as its three-dimensional graph restriction. This identifies the volume-preservation hypothesis for the actual physical-label flow.

noncomputable def EulerGraphInvariantFlow.graphVelocity (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (x : EulerLiftedGradientSpace.Vector3) : EulerLiftedGradientSpace.Vector3

Graph velocity, given by (f (graphLinear k m x)).1.

Equations

• EulerGraphInvariantFlow.graphVelocity k m f x = (f ((EulerGraphInvariantFlow.graphLinear k m) x)).1

theorem EulerGraphInvariantFlow.graphVelocity_trace (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hf : Differentiable ℝ f) (hgraph : ∀ (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) (f z) = 0) (x : EulerLiftedGradientSpace.Vector3) : (LinearMap.trace ℝ EulerLiftedGradientSpace.Vector3) ↑(fderiv ℝ (graphVelocity k m f) x) = (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ f ((graphLinear k m) x))

theorem EulerGraphInvariantFlow.graphVelocity_trace_zero (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hf : Differentiable ℝ f) (hgraph : ∀ (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) (f z) = 0) (hdiv : ∀ (z : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ f z) = 0) (x : EulerLiftedGradientSpace.Vector3) : (LinearMap.trace ℝ EulerLiftedGradientSpace.Vector3) ↑(fderiv ℝ (graphVelocity k m f) x) = 0

noncomputable def EulerGraphInvariantFlow.graphCoefficient (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.Vector3 EulerLiftedGradientSpace.Vector3

Graph coefficient, given by (A.precompLinear (graphLinear k m)).map (fst ℝ Vector3 ℝ).

Equations

• EulerGraphInvariantFlow.graphCoefficient k m T A = SmoothTimeField.map (ContinuousLinearMap.fst ℝ EulerLiftedGradientSpace.Vector3 ℝ) (A.precompLinear (EulerGraphInvariantFlow.graphLinear k m))

@[simp]

theorem EulerGraphInvariantFlow.graphCoefficient_apply (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ((graphCoefficient k m T A).field t) x = ((A.field t) ((graphLinear k m) x)).1

theorem EulerGraphInvariantFlow.graphCoefficient_timeDerivative (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (htime : SmoothTimeField.TimeDerivative T hT A A₁) : SmoothTimeField.TimeDerivative T hT (graphCoefficient k m T A) (graphCoefficient k m T A₁)

theorem EulerGraphInvariantFlow.flowData_tangent (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (r : ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : (graphConstraint k m) ((EulerSmoothBanachFlow.flowData T hT A).velocity r z) = 0

theorem EulerGraphInvariantFlow.graph_flow_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (s t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : graphFlow k m (EulerSmoothBanachFlow.flowData T hT A) s t x = (EulerSmoothBanachFlow.flowData T hT (graphCoefficient k m T A)).flow s t x

theorem EulerGraphInvariantFlow.graph_flow_cover (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (s t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : (EulerSmoothBanachFlow.flowData T hT A).flow s t ((graphLinear k m) x) = (graphLinear k m) ((EulerSmoothBanachFlow.flowData T hT (graphCoefficient k m T A)).flow s t x)

theorem EulerGraphInvariantFlow.graph_displacement_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (EulerSmoothBanachFlow.displacement T hT A (↑t) ((graphLinear k m) x)).1 = EulerSmoothBanachFlow.displacement T hT (graphCoefficient k m T A) (↑t) x

theorem EulerGraphInvariantFlow.graph_forward_contDiff (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (graphFlow k m (EulerSmoothBanachFlow.flowData T hT A) 0 ↑t)

theorem EulerGraphInvariantFlow.graphCoefficient_trace_zero (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) z) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (LinearMap.trace ℝ EulerLiftedGradientSpace.Vector3) ↑(fderiv ℝ (⇑((graphCoefficient k m T A).field t)) x) = 0

theorem EulerGraphInvariantFlow.graph_forward_measurePreserving (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) z) = 0) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MeasurePreserving (graphFlow k m (EulerSmoothBanachFlow.flowData T hT A) 0 ↑t) MeasureTheory.volume MeasureTheory.volume

theorem EulerGraphInvariantFlow.graph_backward_measurePreserving (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) z) = 0) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MeasurePreserving (graphFlow k m (EulerSmoothBanachFlow.flowData T hT A) (↑t) 0) MeasureTheory.volume MeasureTheory.volume

A physical label dilation of a smooth velocity has the conjugate actual flow. Displacement, material velocity and material acceleration are the literal dilations of the corresponding original fields.

noncomputable def EulerSmoothBanachFlow.scaledCoefficient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) : SmoothTimeField (↑(Set.Icc 0 T)) E E

Scaled coefficient, given by (A.precompLinear (ell⁻¹ • ContinuousLinearMap.id ℝ E)).map (ell • ContinuousLinearMap.id ℝ E).

Equations

• EulerSmoothBanachFlow.scaledCoefficient T A ell = SmoothTimeField.map (ell • ContinuousLinearMap.id ℝ E) (A.precompLinear (ell⁻¹ • ContinuousLinearMap.id ℝ E))

@[simp]

theorem EulerSmoothBanachFlow.scaledCoefficient_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) (t : ↑(Set.Icc 0 T)) (x : E) : ((scaledCoefficient T A ell).field t) x = ell • (A.field t) (ell⁻¹ • x)

theorem EulerSmoothBanachFlow.scaledCoefficient_timeDerivative {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (htime : SmoothTimeField.TimeDerivative T hT A A₁) : SmoothTimeField.TimeDerivative T hT (scaledCoefficient T A ell) (scaledCoefficient T A₁ ell)

theorem EulerSmoothBanachFlow.scaled_flow_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) [FiniteDimensional ℝ E] (hell : ell ≠ 0) (s t : ℝ) (x : E) : (flowData T hT (scaledCoefficient T A ell)).flow s t x = ell • (flowData T hT A).flow s t (ell⁻¹ • x)

theorem EulerSmoothBanachFlow.scaled_displacement_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) [FiniteDimensional ℝ E] (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : E) : displacement T hT (scaledCoefficient T A ell) (↑t) x = ell • displacement T hT A (↑t) (ell⁻¹ • x)

theorem EulerSmoothBanachFlow.scaled_materialVelocity_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) [FiniteDimensional ℝ E] (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : E) : EulerSmoothFlowGevrey.materialVelocity T hT (scaledCoefficient T A ell) t x = ell • EulerSmoothFlowGevrey.materialVelocity T hT A t (ell⁻¹ • x)

theorem EulerSmoothBanachFlow.scaledCoefficient_fderiv {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : E) : fderiv ℝ (⇑((scaledCoefficient T A ell).field t)) x = fderiv ℝ (⇑(A.field t)) (ell⁻¹ • x)

theorem EulerSmoothBanachFlow.scaled_accelerationField_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : E) : EulerSmoothFlowGevrey.accelerationField T (scaledCoefficient T A ell) (scaledCoefficient T A₁ ell) t x = ell • EulerSmoothFlowGevrey.accelerationField T A A₁ t (ell⁻¹ • x)

theorem EulerSmoothBanachFlow.scaled_materialAcceleration_eq {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) [FiniteDimensional ℝ E] (A₁ : SmoothTimeField (↑(Set.Icc 0 T)) E E) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : E) : EulerSmoothFlowGevrey.materialAcceleration T hT (scaledCoefficient T A ell) (scaledCoefficient T A₁ ell) t x = ell • EulerSmoothFlowGevrey.materialAcceleration T hT A A₁ t (ell⁻¹ • x)

theorem EulerSmoothBanachFlow.scaledCoefficient_trace_zero {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) E E) (ell : ℝ) (hell : ell ≠ 0) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : E), (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (t : ↑(Set.Icc 0 T)) (x : E) : (LinearMap.trace ℝ E) ↑(fderiv ℝ (⇑((scaledCoefficient T A ell).field t)) x) = 0

theorem EulerGraphInvariantFlow.graph_materialVelocity_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerSmoothFlowGevrey.materialVelocity T hT (graphCoefficient k m T A) t x = (EulerSmoothFlowGevrey.materialVelocity T hT A t ((graphLinear k m) x)).1

theorem EulerGraphInvariantFlow.graph_accelerationField_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerSmoothFlowGevrey.accelerationField T (graphCoefficient k m T A) (graphCoefficient k m T A₁) t x = (EulerSmoothFlowGevrey.accelerationField T A A₁ t ((graphLinear k m) x)).1

theorem EulerGraphInvariantFlow.graph_materialAcceleration_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerSmoothFlowGevrey.materialAcceleration T hT (graphCoefficient k m T A) (graphCoefficient k m T A₁) t x = (EulerSmoothFlowGevrey.materialAcceleration T hT A A₁ t ((graphLinear k m) x)).1

noncomputable def EulerGraphInvariantFlow.physicalCoefficient (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (ell : ℝ) : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.Vector3 EulerLiftedGradientSpace.Vector3

Physical coefficient, given by scaledCoefficient T (graphCoefficient k m T A) ell.

Equations

• EulerGraphInvariantFlow.physicalCoefficient k m T A ell = EulerSmoothBanachFlow.scaledCoefficient T (EulerGraphInvariantFlow.graphCoefficient k m T A) ell

@[simp]

theorem EulerGraphInvariantFlow.physicalCoefficient_apply (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (ell : ℝ) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : ((physicalCoefficient k m T A ell).field t) x = ell • ((A.field t) ((graphLinear k m) (ell⁻¹ • x))).1

theorem EulerGraphInvariantFlow.physicalCoefficient_timeDerivative (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (ell : ℝ) (htime : SmoothTimeField.TimeDerivative T hT A A₁) : SmoothTimeField.TimeDerivative T hT (physicalCoefficient k m T A ell) (physicalCoefficient k m T A₁ ell)

theorem EulerGraphInvariantFlow.physical_flow_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (ell : ℝ) (hell : ell ≠ 0) (s t : ℝ) (x : EulerLiftedGradientSpace.Vector3) : (EulerSmoothBanachFlow.flowData T hT (physicalCoefficient k m T A ell)).flow s t x = ell • ((EulerSmoothBanachFlow.flowData T hT A).flow s t ((graphLinear k m) (ell⁻¹ • x))).1

theorem EulerGraphInvariantFlow.physical_displacement_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (ell : ℝ) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerSmoothBanachFlow.displacement T hT (physicalCoefficient k m T A ell) (↑t) x = ell • (EulerSmoothBanachFlow.displacement T hT A (↑t) ((graphLinear k m) (ell⁻¹ • x))).1

theorem EulerGraphInvariantFlow.physical_materialVelocity_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (ell : ℝ) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerSmoothFlowGevrey.materialVelocity T hT (physicalCoefficient k m T A ell) t x = ell • (EulerSmoothFlowGevrey.materialVelocity T hT A t ((graphLinear k m) (ell⁻¹ • x))).1

theorem EulerGraphInvariantFlow.physical_materialAcceleration_eq (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (ell : ℝ) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : EulerSmoothFlowGevrey.materialAcceleration T hT (physicalCoefficient k m T A ell) (physicalCoefficient k m T A₁ ell) t x = ell • (EulerSmoothFlowGevrey.materialAcceleration T hT A A₁ t ((graphLinear k m) (ell⁻¹ • x))).1

theorem EulerGraphInvariantFlow.physicalCoefficient_trace_zero (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) z) = 0) (ell : ℝ) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (LinearMap.trace ℝ EulerLiftedGradientSpace.Vector3) ↑(fderiv ℝ (⇑((physicalCoefficient k m T A ell).field t)) x) = 0

theorem EulerGraphInvariantFlow.physical_forward_measurePreserving (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (graphConstraint k m) ((A.field t) z) = 0) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) z) = 0) (ell : ℝ) (hell : ell ≠ 0) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MeasurePreserving ((EulerSmoothBanachFlow.flowData T hT (physicalCoefficient k m T A ell)).forward ↑t) MeasureTheory.volume MeasureTheory.volume

A smooth periodic divergence-free cover velocity constructs an actual volume-preserving cylinder flow with continuous inverse.

The actual flow of a periodic cover velocity descends to a genuine continuous cylinder flow with two-sided inverse.

Periodicity of the prescribed velocity gives exact translation equivariance of the constructed global flow, by ODE uniqueness.

theorem EulerBoundedLipschitzFlow.Data.flow_add_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (V : Data E) (c : E) (hc : ∀ (t : ℝ) (x : E), V.velocity t (x + c) = V.velocity t x) (s t : ℝ) (x : E) : V.flow s t (x + c) = V.flow s t x + c

theorem EulerCylinderPeriodicFlow.flow_deck (P : ℝ) (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (s t : ℝ) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : V.flow s t (z.1, ↑c + z.2) = ((V.flow s t z).1, ↑c + (V.flow s t z).2)

noncomputable def EulerCylinderPeriodicFlow.flow (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (s t : ℝ) : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.LiftDomain P

Flow, given by descendMap P (V.flow s t).

Equations

• EulerCylinderPeriodicFlow.flow P V s t = EulerCylinderCoverDescent.descendMap P (V.flow s t)

theorem EulerCylinderPeriodicFlow.flow_cover (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (s t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : flow P V s t (EulerLiftedGradientSpace.coveringMap P z) = EulerLiftedGradientSpace.coveringMap P (V.flow s t z)

theorem EulerCylinderPeriodicFlow.flow_continuous (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (s t : ℝ) : Continuous (flow P V s t)

theorem EulerCylinderPeriodicFlow.flow_initial (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (s : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) : flow P V s s q = q

theorem EulerCylinderPeriodicFlow.flow_inverse (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (s t : ℝ) : Function.LeftInverse (flow P V t s) (flow P V s t)

theorem EulerCylinderPeriodicFlow.flow_cocycle (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (r s t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) : flow P V s t (flow P V r s q) = flow P V r t q

noncomputable def EulerCylinderPeriodicFlow.flowHomeomorph (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (s t : ℝ) : EulerLiftedGradientSpace.LiftDomain P ≃ₜ EulerLiftedGradientSpace.LiftDomain P

Flow homeomorph, bundling toFun, invFun, left_inv, right_inv and the required compatibility proofs.

Equations

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

theorem EulerCylinderPeriodicFlow.forward_joint_continuous (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) : Continuous fun (z : ℝ × EulerLiftedGradientSpace.LiftDomain P) => flow P V 0 z.1 z.2

theorem EulerCylinderPeriodicFlow.backward_joint_continuous (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) : Continuous fun (z : ℝ × EulerLiftedGradientSpace.LiftDomain P) => flow P V z.1 0 z.2

theorem EulerCylinderPeriodicFlow.flow_measurePreserving (P : ℝ) [Fact (0 < P)] (V : EulerBoundedLipschitzFlow.Data EulerLiftedGradientSpace.LiftTangent) (hV : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent), V.velocity t (z.1, ↑c + z.2) = V.velocity t z) (s t : ℝ) (hf : MeasureTheory.MeasurePreserving (V.flow s t) MeasureTheory.volume MeasureTheory.volume) : MeasureTheory.MeasurePreserving (flow P V s t) (EulerLiftedGradientSpace.liftMeasure P) (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerSmoothCylinderFlow.instSmoothCylinderFlow1 : MeasureTheory.volume.IsAddHaarMeasure

theorem EulerSmoothCylinderFlow.velocity_deck (P T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (c : ↥(AddSubgroup.zmultiples P)) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : (EulerSmoothBanachFlow.flowData T hT A).velocity t (z.1, ↑c + z.2) = (EulerSmoothBanachFlow.flowData T hT A).velocity t z

noncomputable def EulerSmoothCylinderFlow.forward (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.LiftDomain P

Forward, given by EulerCylinderPeriodicFlow.flow P (flowData T hT A) 0 t.

Equations

• EulerSmoothCylinderFlow.forward P T hT A t = EulerCylinderPeriodicFlow.flow P (EulerSmoothBanachFlow.flowData T hT A) 0 t

noncomputable def EulerSmoothCylinderFlow.backward (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.LiftDomain P

Backward, given by EulerCylinderPeriodicFlow.flow P (flowData T hT A) t 0.

Equations

• EulerSmoothCylinderFlow.backward P T hT A t = EulerCylinderPeriodicFlow.flow P (EulerSmoothBanachFlow.flowData T hT A) t 0

theorem EulerSmoothCylinderFlow.forward_cover (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : forward P T hT A t (EulerLiftedGradientSpace.coveringMap P z) = EulerLiftedGradientSpace.coveringMap P ((EulerSmoothBanachFlow.flowData T hT A).forward t z)

theorem EulerSmoothCylinderFlow.backward_cover (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : backward P T hT A t (EulerLiftedGradientSpace.coveringMap P z) = EulerLiftedGradientSpace.coveringMap P ((EulerSmoothBanachFlow.flowData T hT A).backward t z)

theorem EulerSmoothCylinderFlow.forward_joint_continuous (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) : Continuous (Function.uncurry (forward P T hT A))

theorem EulerSmoothCylinderFlow.backward_joint_continuous (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) : Continuous (Function.uncurry (backward P T hT A))

theorem EulerSmoothCylinderFlow.backward_forward (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) : Function.LeftInverse (backward P T hT A t) (forward P T hT A t)

theorem EulerSmoothCylinderFlow.forward_backward (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) : Function.RightInverse (backward P T hT A t) (forward P T hT A t)

theorem EulerSmoothCylinderFlow.forward_measurePreserving (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MeasurePreserving (forward P T hT A ↑t) (EulerLiftedGradientSpace.liftMeasure P) (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerSmoothCylinderFlow.backward_measurePreserving (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MeasurePreserving (backward P T hT A ↑t) (EulerLiftedGradientSpace.liftMeasure P) (EulerLiftedGradientSpace.liftMeasure P)

Actual L² composition of any smooth periodic field with the constructed cylinder flow. The outer amplitude is retained.

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderComposition1 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderComposition1 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderComposition2 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderComposition2 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderComposition3 (n : ℕ) : MeasurableSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

The MeasurableSpace (LiftTangent [×n]→L[ℝ] LiftTangent) structure used in smooth cylinder composition.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderComposition3 n = borel (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.instSmoothCylinderComposition4 (n : ℕ) : BorelSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.instSmoothCylinderComposition5 (n : ℕ) : FiniteDimensional ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.composeJet_memLp_and_bound (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hf : ContDiff ℝ (↑⊤) f) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (B R C S : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hC : 0 ≤ C) (hS : 0 ≤ S) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (hLp : ∀ j ≤ n, MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q j) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hNorm : ∀ j ≤ n, (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q j) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * S ^ j * ↑j.factorial ^ 2) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (f ∘ (EulerSmoothBanachFlow.flowData T hT A).forward ↑t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (f ∘ (EulerSmoothBanachFlow.flowData T hT A).forward ↑t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * EulerSmoothFlowGevrey.flowRadius B R T S ^ n * ↑n.factorial ^ 2

The actual composed acceleration field of the constructed periodic flow has L² Gevrey jets with its original source amplitudes.

The actual material acceleration has cylinder L² bounds with the small source amplitudes retained. The product term uses one bounded derivative coefficient and one L² velocity factor.

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp1 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp1 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp2 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp2 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp3 (n : ℕ) : MeasurableSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

The MeasurableSpace (LiftTangent [×n]→L[ℝ] LiftTangent) structure used in smooth cylinder acceleration lᵖ.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp3 n = borel (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp4 (n : ℕ) : BorelSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.instSmoothCylinderAccelerationLp5 (n : ℕ) : FiniteDimensional ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

def EulerSmoothCylinderFlow.accelerationLpRadius (R S S₁ : ℝ) : ℝ

Acceleration Lᵖ radius, given by 4*R+S+S₁.

Equations

• EulerSmoothCylinderFlow.accelerationLpRadius R S S₁ = 4 * R + S + S₁

theorem EulerSmoothCylinderFlow.accelerationField_memLp_and_bound (P T : ℝ) [Fact (0 < P)] (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (B R C S C₁ S₁ : ℝ) (hB : 0 ≤ B) (hR : 0 ≤ R) (hC : 0 ≤ C) (hS : 0 ≤ S) (hC₁ : 0 ≤ C₁) (hS₁ : 0 ≤ S₁) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (hLp : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hNorm : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * S ^ j * ↑j.factorial ^ 2) (hLp₁ : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A₁.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hNorm₁ : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A₁.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C₁ * S₁ ^ j * ↑j.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothFlowGevrey.accelerationField T A A₁ t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothFlowGevrey.accelerationField T A A₁ t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ (C₁ + 3 * B * R * C) * accelerationLpRadius R S S₁ ^ n * ↑n.factorial ^ 2

theorem EulerSmoothCylinderFlow.accelerationField_deck (P T : ℝ) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hA₁ : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A₁.field t) (z.1, ↑c + z.2) = (A₁.field t) z) (t : ↑(Set.Icc 0 T)) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothFlowGevrey.accelerationField T A A₁ t (z.1, ↑c + z.2) = EulerSmoothFlowGevrey.accelerationField T A A₁ t z

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderAccelerationComposition1 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderAccelerationComposition1 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderAccelerationComposition2 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderAccelerationComposition2 n = inferInstance

noncomputable def EulerSmoothCylinderFlow.materialAccelerationJet (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent

Material acceleration jet, given by jetSeries P (materialAcceleration T hT A A₁ t) q n.

Equations

• EulerSmoothCylinderFlow.materialAccelerationJet P T hT A A₁ t q n = EulerCylinderCoverDescent.jetSeries P (EulerSmoothFlowGevrey.materialAcceleration T hT A A₁ t) q n

theorem EulerSmoothCylinderFlow.materialAccelerationJet_local (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hA₁ : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A₁.field t) (z.1, ↑c + z.2) = (A₁.field t) z) (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : materialAccelerationJet P T hT A A₁ t q n = iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P (EulerCylinderCoverDescent.descend P (EulerSmoothFlowGevrey.materialAcceleration T hT A A₁ t)) q) 0

theorem EulerSmoothCylinderFlow.materialAccelerationJet_memLp_and_bound (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hA₁ : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A₁.field t) (z.1, ↑c + z.2) = (A₁.field t) z) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (B R C S C₁ S₁ : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hC : 0 ≤ C) (hS : 0 ≤ S) (hC₁ : 0 ≤ C₁) (hS₁ : 0 ≤ S₁) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (hLp : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hNorm : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * S ^ j * ↑j.factorial ^ 2) (hLp₁ : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A₁.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hNorm₁ : ∀ (t : ↑(Set.Icc 0 T)) (j : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A₁.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C₁ * S₁ ^ j * ↑j.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => materialAccelerationJet P T hT A A₁ t q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => materialAccelerationJet P T hT A A₁ t q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ (C₁ + 3 * B * R * C) * EulerSmoothFlowGevrey.flowRadius B R T (accelerationLpRadius R S S₁) ^ n * ↑n.factorial ^ 2

Actual periodic displacement jets and their differentiated integral equation. The real covering displacement is periodic, so its descent is a vector-valued field, including its angular displacement component.

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderJets1 (n : ℕ) : MeasurableSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

The MeasurableSpace (LiftTangent [×n]→L[ℝ] LiftTangent) structure used in smooth cylinder jets.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderJets1 n = borel (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.instSmoothCylinderJets2 (n : ℕ) : BorelSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

noncomputable def EulerSmoothCylinderFlow.velocityCover (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent

Velocity cover, given by A.field (projIcc 0 T hT t).

Equations

• EulerSmoothCylinderFlow.velocityCover T hT A t = ⇑(A.field (Set.projIcc 0 T hT t))

noncomputable def EulerSmoothCylinderFlow.forwardCover (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent

Forward cover, given by (flowData T hT A).forward (projIcc 0 T hT t).

Equations

• EulerSmoothCylinderFlow.forwardCover T hT A t = (EulerSmoothBanachFlow.flowData T hT A).forward ↑(Set.projIcc 0 T hT t)

theorem EulerSmoothCylinderFlow.forwardCover_deck (P T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : forwardCover T hT A t (z.1, ↑c + z.2) = ((forwardCover T hT A t z).1, ↑c + (forwardCover T hT A t z).2)

theorem EulerSmoothCylinderFlow.coverDisplacement_deck (P T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothBanachFlow.displacement T hT A t (z.1, ↑c + z.2) = EulerSmoothBanachFlow.displacement T hT A t z

noncomputable def EulerSmoothCylinderFlow.displacement (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.LiftTangent

Displacement, given by descend P (EulerSmoothBanachFlow.displacement T hT A t).

Equations

• EulerSmoothCylinderFlow.displacement P T hT A t = EulerCylinderCoverDescent.descend P (EulerSmoothBanachFlow.displacement T hT A t)

noncomputable def EulerSmoothCylinderFlow.displacementJet (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent

Displacement jet, given by jetSeries P (EulerSmoothBanachFlow.displacement T hT A t) q n.

Equations

• EulerSmoothCylinderFlow.displacementJet P T hT A t q n = EulerCylinderCoverDescent.jetSeries P (EulerSmoothBanachFlow.displacement T hT A t) q n

noncomputable def EulerSmoothCylinderFlow.compositionJet (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent

Composition jet as an element of LiftTangent [×n]→L[ℝ] LiftTangent.

Equations

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

theorem EulerSmoothCylinderFlow.displacement_cover (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : displacement P T hT A t (EulerLiftedGradientSpace.coveringMap P z) = EulerSmoothBanachFlow.displacement T hT A t z

theorem EulerSmoothCylinderFlow.displacement_smooth (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (displacement P T hT A t) q)

theorem EulerSmoothCylinderFlow.displacementJet_local (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : displacementJet P T hT A t q n = iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P (displacement P T hT A t) q) 0

theorem EulerSmoothCylinderFlow.compositionJet_eq (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : compositionJet P T hT A t q n = iteratedFDeriv ℝ n (velocityCover T hT A t ∘ forwardCover T hT A t) (EulerCylinderCoverDescent.sectionPoint P q)

theorem EulerSmoothCylinderFlow.compositionJet_path (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : compositionJet P T hT A t q n = EulerVolterraConvolution.extendPath T hT (EulerSmoothBanachFlow.velocityJetPath T hT A n (EulerCylinderCoverDescent.sectionPoint P q)) t

theorem EulerSmoothCylinderFlow.displacementJet_path (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (t : ℝ) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : displacementJet P T hT A t q n = EulerVolterraConvolution.extendPath T hT (EulerSmoothBanachFlow.displacementJetPath T hT A n (EulerCylinderCoverDescent.sectionPoint P q)) t

theorem EulerSmoothCylinderFlow.displacementJet_integral (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.LiftDomain P) (n : ℕ) : displacementJet P T hT A (↑t) q n = ∫ (s : ℝ) in 0..↑t, compositionJet P T hT A s q n

theorem EulerSmoothCylinderFlow.velocityJetPath_label_continuous (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (n : ℕ) : Continuous (EulerSmoothBanachFlow.velocityJetPath T hT A n)

theorem EulerSmoothCylinderFlow.displacementJetPath_label_continuous (T : ℝ) (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (n : ℕ) : Continuous (EulerSmoothBanachFlow.displacementJetPath T hT A n)

theorem EulerSmoothCylinderFlow.compositionJet_joint_measurable (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (n : ℕ) : Measurable fun (z : ℝ × EulerLiftedGradientSpace.LiftDomain P) => compositionJet P T hT A z.1 z.2 n

theorem EulerSmoothCylinderFlow.displacementJet_joint_measurable (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (n : ℕ) : Measurable fun (z : ℝ × EulerLiftedGradientSpace.LiftDomain P) => displacementJet P T hT A z.1 z.2 n

The actual periodic flow displacement has simultaneous uniform and L² Gevrey bounds. The L² estimate uses the cylinder's own Haar measure and the differentiated equation of the constructed flow.

The all-order L² step for a volume-preserving flow. The spatial base may be a periodic cylinder. The output is the actual time integral of the finite Taylor composition; identifying it with the displacement jet uses the already constructed flow's differentiated integral equation.

theorem EulerGevreyFlowLpIntegration.integrated_composition_bound {X : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (φ : ℝ → X → X) (hφ : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MeasurePreserving (φ t) μ μ) (P : ℝ → X → FormalMultilinearSeries ℝ E E) (Q : ℝ → X → FormalMultilinearSeries ℝ E F) (n : ℕ) (hm : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × X) => (Q p.1 (φ p.1 p.2)).taylorComp (P p.1 p.2) n) ((MeasureTheory.volume.restrict (Set.Icc 0 T)).prod μ)) (A B R S : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hR : 0 ≤ R) (hS : 0 ≤ S) (hQLp : ∀ t ∈ Set.Icc 0 T, ∀ j ≤ n, MeasureTheory.MemLp (fun (x : X) => Q t x j) 2 μ) (hQ : ∀ t ∈ Set.Icc 0 T, ∀ j ≤ n, (MeasureTheory.eLpNorm (fun (x : X) => Q t x j) 2 μ).toReal ≤ A * S ^ j * ↑j.factorial ^ 2) (hP : ∀ t ∈ Set.Icc 0 T, ∀ (j : ℕ), 0 < j → j ≤ n → ∀ (x : X), ‖P t x j‖ ≤ B * R ^ j * ↑j.factorial ^ 2) : MeasureTheory.MemLp (fun (x : X) => ∫ (t : ℝ) in 0..T, (Q t (φ t x)).taylorComp (P t x) n) 2 μ ∧ (MeasureTheory.eLpNorm (fun (x : X) => ∫ (t : ℝ) in 0..T, (Q t (φ t x)).taylorComp (P t x) n) 2 μ).toReal ≤ T * A * (R * (B * S + 2)) ^ n * ↑n.factorial ^ 2

Uniform positive inner-jet bounds and the outer L² bounds imply an L² bound for the actual integrated composition at every finite order.

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderGevrey1 (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedAddCommGroup (LiftTangent [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderGevrey1 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderGevrey2 (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

Cache the standard NormedSpace ℝ (LiftTangent [×n]→L[ℝ] LiftTangent) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderGevrey2 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderGevrey3 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderGevrey3 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderGevrey4 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderGevrey4 n = inferInstance

@[instance_reducible]

noncomputable def EulerSmoothCylinderFlow.instSmoothCylinderGevrey5 (n : ℕ) : MeasurableSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

The MeasurableSpace (LiftTangent [×n]→L[ℝ] LiftTangent) structure used in smooth cylinder gevrey.

Equations

• EulerSmoothCylinderFlow.instSmoothCylinderGevrey5 n = borel (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.instSmoothCylinderGevrey6 (n : ℕ) : BorelSpace (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.instSmoothCylinderGevrey7 (n : ℕ) : FiniteDimensional ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent)

theorem EulerSmoothCylinderFlow.displacementJet_bound (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (B R : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 T)) (q : EulerLiftedGradientSpace.LiftDomain P) : ‖displacementJet P T hT A (↑t) q n‖ ≤ B * ↑t * (4 * R) ^ n * ↑n.factorial ^ 2

theorem EulerSmoothCylinderFlow.compositionJet_memLp_and_bound (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (B R C S : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hC : 0 ≤ C) (hS : 0 ≤ S) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (hLp : ∀ (t : ↑(Set.Icc 0 T)), ∀ j ≤ n, MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hNorm : ∀ (t : ↑(Set.Icc 0 T)), ∀ j ≤ n, (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * S ^ j * ↑j.factorial ^ 2) (t : ℝ) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => compositionJet P T hT A t q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => compositionJet P T hT A t q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * EulerSmoothFlowGevrey.flowRadius B R T S ^ n * ↑n.factorial ^ 2

theorem EulerSmoothCylinderFlow.displacementJet_memLp_and_bound (P T : ℝ) [Fact (0 < P)] (hT : 0 ≤ T) (A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent) (hA : ∀ (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (A.field t) (z.1, ↑c + z.2) = (A.field t) z) (hdiv : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftTangent), (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(A.field t)) x) = 0) (B R C S : ℝ) (hB : 0 ≤ B) (hR : 0 < R) (hC : 0 ≤ C) (hS : 0 ≤ S) (hsmall : B * R * T ≤ 1 / 8) (hb : ∀ (n : ℕ), ‖A.jet n‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (hLp : ∀ (t : ↑(Set.Icc 0 T)), ∀ j ≤ n, MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hNorm : ∀ (t : ↑(Set.Icc 0 T)), ∀ j ≤ n, (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(A.field t)) q j) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * S ^ j * ↑j.factorial ^ 2) (t : ↑(Set.Icc 0 T)) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => displacementJet P T hT A (↑t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => displacementJet P T hT A (↑t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ ↑t * C * EulerSmoothFlowGevrey.flowRadius B R T S ^ n * ↑n.factorial ^ 2

@[instance_reducible]

noncomputable def EulerPhysicalGraphFlowBounds.instPhysicalGraphFlowBounds1 (n : ℕ) : NormedAddCommGroup (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedAddCommGroup (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerPhysicalGraphFlowBounds.instPhysicalGraphFlowBounds1 n = inferInstance

@[instance_reducible]

noncomputable def EulerPhysicalGraphFlowBounds.instPhysicalGraphFlowBounds2 (n : ℕ) : NormedSpace ℝ (BoundedContinuousFunction EulerLiftedGradientSpace.LiftTangent (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] EulerLiftedGradientSpace.LiftTangent))

Cache the standard NormedSpace ℝ (LiftTangent →ᵇ (LiftTangent [×n]→L[ℝ] LiftTangent)) instance to shorten typeclass synthesis.

Equations

• EulerPhysicalGraphFlowBounds.instPhysicalGraphFlowBounds2 n = inferInstance

structure EulerPhysicalGraphFlowBounds.Data (P T : ℝ) [Fact (0 < P)] : Type

Data, collecting time_nonneg, A, A₁, time_derivative, periodic, periodic_time and their compatibility conditions.

• time_nonneg : 0 ≤ T
• A : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent

  A of Data, of type SmoothTimeField (Icc (0 : ℝ) T) LiftTangent LiftTangent.

• A₁ : SmoothTimeField (↑(Set.Icc 0 T)) EulerLiftedGradientSpace.LiftTangent EulerLiftedGradientSpace.LiftTangent

  A₁ of Data, of type SmoothTimeField (Icc (0 : ℝ) T) LiftTangent LiftTangent.

• time_derivative : SmoothTimeField.TimeDerivative T ⋯ self.A self.A₁
• periodic (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent) : (self.A.field t) (z.1, ↑c + z.2) = (self.A.field t) z
• periodic_time (c : ↥(AddSubgroup.zmultiples P)) (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent) : (self.A₁.field t) (z.1, ↑c + z.2) = (self.A₁.field t) z
• divergence (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent) : (LinearMap.trace ℝ EulerLiftedGradientSpace.LiftTangent) ↑(fderiv ℝ (⇑(self.A.field t)) z) = 0
• B : ℝ

  Bound parameter of Data, of type ℝ.

• R : ℝ

  Radius parameter of Data, of type ℝ.

• C : ℝ

  Bound coefficient of Data, of type ℝ.

• S : ℝ

  Parameter S of Data, of type ℝ.

• C₁ : ℝ

  First-derivative bound coefficient of Data, of type ℝ.

• S₁ : ℝ

  Parameter S₁ of Data, of type ℝ.

• B_nonneg : 0 ≤ self.B
• R_pos : 0 < self.R
• C_nonneg : 0 ≤ self.C
• S_nonneg : 0 ≤ self.S
• C₁_nonneg : 0 ≤ self.C₁
• S₁_nonneg : 0 ≤ self.S₁
• small : self.B * self.R * T ≤ 1 / 8
• sup_bound (n : ℕ) : ‖self.A.jet n‖ ≤ self.B * self.R ^ n * ↑n.factorial ^ 2
• integrable (t : ↑(Set.Icc 0 T)) (n : ℕ) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(self.A.field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)
• lp_bound (t : ↑(Set.Icc 0 T)) (n : ℕ) : (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(self.A.field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ self.C * self.S ^ n * ↑n.factorial ^ 2
• integrable_time (t : ↑(Set.Icc 0 T)) (n : ℕ) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(self.A₁.field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)
• lp_bound_time (t : ↑(Set.Icc 0 T)) (n : ℕ) : (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (⇑(self.A₁.field t)) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ self.C₁ * self.S₁ ^ n * ↑n.factorial ^ 2

def EulerPhysicalGraphFlowBounds.Data.velocityRadius {P T : ℝ} [Fact (0 < P)] (G : Data P T) : ℝ

Velocity radius, given by flowRadius G.B G.R T G.S.

Equations

• G.velocityRadius = EulerSmoothFlowGevrey.flowRadius G.B G.R T G.S

def EulerPhysicalGraphFlowBounds.Data.accelerationRadius {P T : ℝ} [Fact (0 < P)] (G : Data P T) : ℝ

Acceleration radius, given by flowRadius G.B G.R T (4*G.R+G.S+G.S₁).

Equations

• G.accelerationRadius = EulerSmoothFlowGevrey.flowRadius G.B G.R T (4 * G.R + G.S + G.S₁)

def EulerPhysicalGraphFlowBounds.Data.accelerationAmplitude {P T : ℝ} [Fact (0 < P)] (G : Data P T) : ℝ

Acceleration amplitude, given by G.C₁+3*G.B*G.R*G.C.

Equations

• G.accelerationAmplitude = G.C₁ + 3 * G.B * G.R * G.C

theorem EulerPhysicalGraphFlowBounds.Data.velocityRadius_nonneg {P T : ℝ} [Fact (0 < P)] (G : Data P T) : 0 ≤ G.velocityRadius

theorem EulerPhysicalGraphFlowBounds.Data.accelerationRadius_nonneg {P T : ℝ} [Fact (0 < P)] (G : Data P T) : 0 ≤ G.accelerationRadius

theorem EulerPhysicalGraphFlowBounds.Data.accelerationAmplitude_nonneg {P T : ℝ} [Fact (0 < P)] (G : Data P T) : 0 ≤ G.accelerationAmplitude

theorem EulerPhysicalGraphFlowBounds.Data.displacement_cylinder_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (n : ℕ) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothBanachFlow.displacement T ⋯ G.A ↑t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothBanachFlow.displacement T ⋯ G.A ↑t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ T * G.C * G.velocityRadius ^ n * ↑n.factorial ^ 2

theorem EulerPhysicalGraphFlowBounds.Data.velocity_periodic {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothFlowGevrey.materialVelocity T ⋯ G.A t (z.1, ↑c + z.2) = EulerSmoothFlowGevrey.materialVelocity T ⋯ G.A t z

theorem EulerPhysicalGraphFlowBounds.Data.velocity_smooth {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (EulerSmoothFlowGevrey.materialVelocity T ⋯ G.A t)

theorem EulerPhysicalGraphFlowBounds.Data.velocity_cylinder_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (n : ℕ) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothFlowGevrey.materialVelocity T ⋯ G.A t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothFlowGevrey.materialVelocity T ⋯ G.A t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ G.C * G.velocityRadius ^ n * ↑n.factorial ^ 2

theorem EulerPhysicalGraphFlowBounds.Data.acceleration_periodic {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothFlowGevrey.materialAcceleration T ⋯ G.A G.A₁ t (z.1, ↑c + z.2) = EulerSmoothFlowGevrey.materialAcceleration T ⋯ G.A G.A₁ t z

theorem EulerPhysicalGraphFlowBounds.Data.acceleration_smooth {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ (↑⊤) (EulerSmoothFlowGevrey.materialAcceleration T ⋯ G.A G.A₁ t)

theorem EulerPhysicalGraphFlowBounds.Data.acceleration_cylinder_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (t : ↑(Set.Icc 0 T)) (n : ℕ) : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothFlowGevrey.materialAcceleration T ⋯ G.A G.A₁ t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P (EulerSmoothFlowGevrey.materialAcceleration T ⋯ G.A G.A₁ t) q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ G.accelerationAmplitude * G.accelerationRadius ^ n * ↑n.factorial ^ 2

noncomputable def EulerPhysicalGraphFlowBounds.Data.displacementField {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerLiftedGradientSpace.Vector3

Displacement field, constructed using physicalField.

Equations

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

noncomputable def EulerPhysicalGraphFlowBounds.Data.velocityField {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerLiftedGradientSpace.Vector3

Velocity field, constructed using physicalField.

Equations

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

noncomputable def EulerPhysicalGraphFlowBounds.Data.accelerationFieldL2 {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) : EulerLpTranslation.SmoothL2Field EulerLiftedGradientSpace.Vector3

Acceleration field L², constructed using physicalField.

Equations

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

theorem EulerPhysicalGraphFlowBounds.Data.displacementField_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) : (G.displacementField k m ell hell t).HasJetBound (√(2 / P + 2 * P) * (T * G.C) * (1 + G.velocityRadius)) (ell⁻¹ * (4 * G.velocityRadius * EulerCylinderGraphGevrey.graphFactor k m))

theorem EulerPhysicalGraphFlowBounds.Data.velocityField_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) : (G.velocityField k m ell hell t).HasJetBound (√(2 / P + 2 * P) * G.C * (1 + G.velocityRadius)) (ell⁻¹ * (4 * G.velocityRadius * EulerCylinderGraphGevrey.graphFactor k m))

theorem EulerPhysicalGraphFlowBounds.Data.accelerationField_bound {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (t : ↑(Set.Icc 0 T)) : (G.accelerationFieldL2 k m ell hell t).HasJetBound (√(2 / P + 2 * P) * G.accelerationAmplitude * (1 + G.accelerationRadius)) (ell⁻¹ * (4 * G.accelerationRadius * EulerCylinderGraphGevrey.graphFactor k m))

theorem EulerPhysicalGraphFlowBounds.Data.displacementField_eq {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (G.displacementField k m ell hell t).field x = EulerSmoothBanachFlow.displacement T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell) (↑t) x

theorem EulerPhysicalGraphFlowBounds.Data.velocityField_eq {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (G.velocityField k m ell hell t).field x = EulerSmoothFlowGevrey.materialVelocity T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell) t x

theorem EulerPhysicalGraphFlowBounds.Data.accelerationField_eq {P T : ℝ} [Fact (0 < P)] (G : Data P T) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (hgraph : ∀ (t : ↑(Set.Icc 0 T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0) (ell : ℝ) (hell : 0 < ell) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.Vector3) : (G.accelerationFieldL2 k m ell hell t).field x = EulerSmoothFlowGevrey.materialAcceleration T ⋯ (EulerGraphInvariantFlow.physicalCoefficient k m T G.A ell) (EulerGraphInvariantFlow.physicalCoefficient k m T G.A₁ ell) t x