Canonical graph restrictions need no additional representative or regularity assumptions beyond the actual all-order tower.

Actual spatial L² restrictions of smooth cylinder fields. The bound is uniform over every continuous phase graph, including arbitrarily high oscillation frequencies.

theorem EulerCylinderGraphTrace.graph_memLp_of_representatives (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (u v : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hv : ↑↑v =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) f) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.Vector3) => f (x, θ x)) 2 MeasureTheory.volume

noncomputable def EulerCylinderGraphTrace.graphRealization (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (u v : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hv : ↑↑v =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) f) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) : ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)

The actual L² class of the field on the prescribed phase graph.

Equations

• EulerCylinderGraphTrace.graphRealization P f hf u v hu hv θ hθ = MeasureTheory.MemLp.toLp (fun (x : EulerLiftedGradientSpace.Vector3) => f (x, θ x)) ⋯

theorem EulerCylinderGraphTrace.graphRealization_ae (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (u v : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hv : ↑↑v =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) f) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) : ↑↑(graphRealization P f hf u v hu hv θ hθ) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => f (x, θ x)

theorem EulerCylinderGraphTrace.graph_norm_sq_le (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (u v : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hv : ↑↑v =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) f) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (w : ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)) (hw : ↑↑w =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => f (x, θ x)) : ‖w‖ ^ 2 ≤ 2 / P * ‖u‖ ^ 2 + 2 * P * ‖v‖ ^ 2

Any L² representative of this same graph satisfies the genuine trace bound.

theorem EulerCylinderGraphTrace.graphRealization_norm_sq_le (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f x)) (u v : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hv : ↑↑v =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) f) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) : ‖graphRealization P f hf u v hu hv θ hθ‖ ^ 2 ≤ 2 / P * ‖u‖ ^ 2 + 2 * P * ‖v‖ ^ 2

Every smooth representative of a genuine all-order field tower has continuous spatial L² restrictions, including all cylinder derivative words. The graph estimate loses one angular derivative, with no frequency factor.

Restriction to a fixed continuous phase graph preserves time continuity in actual spatial L². The proof uses the uniform trace estimate for differences.

noncomputable def EulerCylinderGraphTrace.graphPathValue (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (u v : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (f : K → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : K) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hu : ∀ (t : K), ↑↑(u t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (hv : ∀ (t : K), ↑↑(v t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (f t)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (t : K) : ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)

Graph path value, given by graphRealization P (f t) (hf t) (u t) (v t) (hu t) (hv t) θ hθ.

Equations

• EulerCylinderGraphTrace.graphPathValue P u v f hf hu hv θ hθ t = EulerCylinderGraphTrace.graphRealization P (f t) ⋯ (u t) (v t) ⋯ ⋯ θ hθ

theorem EulerCylinderGraphTrace.graphPathValue_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (u v : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (f : K → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : K) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hu : ∀ (t : K), ↑↑(u t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (hv : ∀ (t : K), ↑↑(v t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (f t)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (t : K) : ↑↑(graphPathValue P u v f hf hu hv θ hθ t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => f t (x, θ x)

theorem EulerCylinderGraphTrace.graphPathValue_sub_norm_sq_le (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (u v : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (f : K → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : K) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hu : ∀ (t : K), ↑↑(u t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (hv : ∀ (t : K), ↑↑(v t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (f t)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (t s : K) : ‖graphPathValue P u v f hf hu hv θ hθ t - graphPathValue P u v f hf hu hv θ hθ s‖ ^ 2 ≤ 2 / P * ‖u t - u s‖ ^ 2 + 2 * P * ‖v t - v s‖ ^ 2

theorem EulerCylinderGraphTrace.graphPathValue_continuous (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (u v : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (f : K → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : K) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hu : ∀ (t : K), ↑↑(u t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (hv : ∀ (t : K), ↑↑(v t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (f t)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) : Continuous (graphPathValue P u v f hf hu hv θ hθ)

noncomputable def EulerCylinderGraphTrace.graphPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] (u v : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (f : K → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : K) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hu : ∀ (t : K), ↑↑(u t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (hv : ∀ (t : K), ↑↑(v t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (f t)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) : C(K, ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume))

The continuous spatial L² path is constructed from the actual cylinder path and its actual angular derivative.

Equations

• EulerCylinderGraphTrace.graphPath P u v f hf hu hv θ hθ = { toFun := EulerCylinderGraphTrace.graphPathValue P u v f hf hu hv θ hθ, continuous_toFun := ⋯ }

noncomputable def EulerAllOrderCorrectionData.FieldTower.derivativeWordPath {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (s n : ℕ) (w : Fin n → Fin 4) (hn : n ≤ s) : C(↑(Set.Icc 0 T), ↥(EulerLiftedGradientSpace.LiftL2 P))

The prescribed derivative coordinate is a genuine continuous L² path.

Equations

• A.derivativeWordPath s n w hn = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.wordOperator P ⟨⟨n, ⋯⟩, w⟩)) (A.realization s)

theorem EulerAllOrderCorrectionData.FieldTower.derivativeWordPath_ae {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (f : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hrep : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (s n : ℕ) (w : Fin n → Fin 4) (hn : n ≤ s) (t : ↑(Set.Icc 0 T)) : ↑↑((A.derivativeWordPath s n w hn) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerCylinderSobolev.iteratedFieldDerivative P w (f t)

theorem EulerAllOrderCorrectionData.FieldTower.derivativeWordPath_norm_le {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (s n : ℕ) (w : Fin n → Fin 4) (hn : n ≤ s) (t : ↑(Set.Icc 0 T)) : ‖(A.derivativeWordPath s n w hn) t‖ ≤ ‖(A.realization s) t‖

theorem EulerAllOrderCorrectionData.FieldTower.graphWord_angular_ae {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (f : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hrep : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) : ↑↑((A.derivativeWordPath (n + 1) (n + 1) (Fin.cons 0 w) ⋯) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (EulerCylinderSobolev.iteratedFieldDerivative P w (f t))

The actual angular derivative used by the graph trace is another coordinate of the same all-order tower.

noncomputable def EulerAllOrderCorrectionData.FieldTower.graphWordPath {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (f : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hrep : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume))

Graph restriction of an arbitrary actual cylinder derivative word, constructed directly as a continuous spatial L² path.

Equations

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

theorem EulerAllOrderCorrectionData.FieldTower.graphWordPath_ae {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (f : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hrep : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) : ↑↑((A.graphWordPath f hf hrep θ hθ n w) t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w (f t) (x, θ x)

theorem EulerAllOrderCorrectionData.FieldTower.graphWordPath_norm_sq_le {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (f : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hrep : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) : ‖(A.graphWordPath f hf hrep θ hθ n w) t‖ ^ 2 ≤ (2 / P + 2 * P) * ‖(A.realization (n + 1)) t‖ ^ 2

A genuine cylinder L² time derivative, together with its genuine angular derivative, remains a genuine spatial L² derivative on every fixed phase graph.

The graph trace estimate applies to the actual affine remainder in a derivative quotient, with the same constants for all phase frequencies.

theorem EulerCylinderGraphTrace.affine_representative_ae {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) (u : Fin 3 → ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 μ)) (f : Fin 3 → X → EulerLiftedGradientSpace.Vector3) (hu : ∀ (i : Fin 3), ↑↑(u i) =ᵐ[μ] f i) (a : ℝ) : ↑↑(a • (u 1 - u 0) - u 2) =ᵐ[μ] fun (x : X) => a • (f 1 x - f 0 x) - f 2 x

theorem EulerCylinderGraphTrace.affine_fieldDerivative (P : ℝ) (f : Fin 3 → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f i) x)) (a : ℝ) (z : EulerLiftedGradientSpace.LiftDomain P) : EulerTransportDerivatives.fieldDerivative P (0, 1) (fun (x : EulerLiftedGradientSpace.LiftDomain P) => a • (f 1 x - f 0 x) - f 2 x) z = a • (EulerTransportDerivatives.fieldDerivative P (0, 1) (f 1) z - EulerTransportDerivatives.fieldDerivative P (0, 1) (f 0) z) - EulerTransportDerivatives.fieldDerivative P (0, 1) (f 2) z

theorem EulerCylinderGraphTrace.graph_affine_norm_sq_le (P : ℝ) [Fact (0 < P)] (f : Fin 3 → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f i) x)) (u v : Fin 3 → ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu : ∀ (i : Fin 3), ↑↑(u i) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f i) (hv : ∀ (i : Fin 3), ↑↑(v i) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (f i)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (w : Fin 3 → ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)) (hw : ∀ (i : Fin 3), ↑↑(w i) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => f i (x, θ x)) (a : ℝ) : ‖a • (w 1 - w 0) - w 2‖ ^ 2 ≤ 2 / P * ‖a • (u 1 - u 0) - u 2‖ ^ 2 + 2 * P * ‖a • (v 1 - v 0) - v 2‖ ^ 2

theorem EulerCylinderGraphTrace.graph_hasDerivWithinAt (P : ℝ) [Fact (0 < P)] (u v : ℝ → ↥(EulerLiftedGradientSpace.LiftL2 P)) (f : ℝ → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (r : ℝ) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f r) x)) (hu : ∀ (r : ℝ), ↑↑(u r) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f r) (hv : ∀ (r : ℝ), ↑↑(v r) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) (f r)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (w : ℝ → ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)) (hw : ∀ (r : ℝ), ↑↑(w r) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => f r (x, θ x)) (g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g x)) (u' v' : ↥(EulerLiftedGradientSpace.LiftL2 P)) (hu' : ↑↑u' =ᵐ[EulerLiftedGradientSpace.liftMeasure P] g) (hv' : ↑↑v' =ᵐ[EulerLiftedGradientSpace.liftMeasure P] EulerTransportDerivatives.fieldDerivative P (0, 1) g) (w' : ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume)) (hw' : ↑↑w' =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => g (x, θ x)) (s : Set ℝ) (t : ℝ) (hdu : HasDerivWithinAt u u' s t) (hdv : HasDerivWithinAt v v' s t) : HasDerivWithinAt w w' s t

Genuine Sobolev time derivatives of coherent towers pass to actual spatial L² derivatives after restriction to any fixed phase graph.

theorem EulerAllOrderCorrectionData.FieldTower.graphWordPath_hasDerivWithinAt {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) (f g : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hg : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (g t) x)) (ha : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (hb : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(B.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] g t) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (hT : 0 ≤ T) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) (hd : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (A.realization (n + 1))) ((B.realization (n + 1)) t) (Set.Icc 0 T) ↑t) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (A.graphWordPath f hf ha θ hθ n w)) ((B.graphWordPath g hg hb θ hθ n w) t) (Set.Icc 0 T) ↑t

theorem EulerAllOrderCorrectionData.FieldTower.graphWordPath_hasDerivAt {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) (f g : ↑(Set.Icc 0 T) → EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (f t) x)) (hg : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (g t) x)) (ha : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(A.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f t) (hb : ∀ (t : ↑(Set.Icc 0 T)), ↑↑(B.field t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] g t) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (hT : 0 ≤ T) (n : ℕ) (w : Fin n → Fin 4) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (hd : HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.realization (n + 1))) ((B.realization (n + 1)) ⟨t, ⋯⟩) t) : HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.graphWordPath f hf ha θ hθ n w)) ((B.graphWordPath g hg hb θ hθ n w) ⟨t, ⋯⟩) t

A genuine derivative at one Sobolev order gives the same derivative at all lower orders of the coherent towers.

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.restrictionGroup {P : ℝ} [Fact (0 < P)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

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

Equations

• EulerAllOrderCorrectionData.FieldTower.restrictionGroup q = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.restrictionSpace {P : ℝ} [Fact (0 < P)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

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

Equations

• EulerAllOrderCorrectionData.FieldTower.restrictionSpace q = inferInstance

@[instance_reducible]

noncomputable def EulerAllOrderCorrectionData.FieldTower.restrictionTopology {P : ℝ} [Fact (0 < P)] (q : ℕ) : TopologicalSpace ↥(EulerCylinderSobolevSpace.SobolevSpace P q)

Cache the standard TopologicalSpace (SobolevSpace P q) instance to shorten typeclass synthesis.

Equations

• EulerAllOrderCorrectionData.FieldTower.restrictionTopology q = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

theorem EulerAllOrderCorrectionData.FieldTower.realization_hasDerivWithinAt_of_le {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) {p q : ℕ} (h : q ≤ p) (hT : 0 ≤ T) (t : ↑(Set.Icc 0 T)) (hd : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (A.realization p)) ((B.realization p) t) (Set.Icc 0 T) ↑t) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (A.realization q)) ((B.realization q) t) (Set.Icc 0 T) ↑t

theorem EulerAllOrderCorrectionData.FieldTower.realization_hasDerivAt_of_le {P T : ℝ} [Fact (0 < P)] (A B : FieldTower P T) {p q : ℕ} (h : q ≤ p) (hT : 0 ≤ T) (t : ↑(Set.Icc 0 T)) (hd : HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.realization p)) ((B.realization p) t) ↑t) : HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.realization q)) ((B.realization q) t) ↑t

noncomputable def EulerAllOrderCorrectionData.FieldTower.canonicalGraphWordPath {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) : C(↑(Set.Icc 0 T), ↥(MeasureTheory.Lp EulerLiftedGradientSpace.Vector3 2 MeasureTheory.volume))

Canonical graph word path, given by A.graphWordPath A.pointField A.pointField_smooth A.pointField_ae θ hθ n w.

Equations

• A.canonicalGraphWordPath θ hθ n w = A.graphWordPath A.pointField ⋯ ⋯ θ hθ n w

theorem EulerAllOrderCorrectionData.FieldTower.canonicalGraphWordPath_ae {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) : ↑↑((A.canonicalGraphWordPath θ hθ n w) t) =ᵐ[MeasureTheory.volume] fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderSobolev.iteratedFieldDerivative P w (A.pointField t) (x, θ x)

theorem EulerAllOrderCorrectionData.FieldTower.canonicalGraphWordPath_norm_sq_le {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (t : ↑(Set.Icc 0 T)) : ‖(A.canonicalGraphWordPath θ hθ n w) t‖ ^ 2 ≤ (2 / P + 2 * P) * ‖(A.realization (n + 1)) t‖ ^ 2

theorem EulerAllOrderCorrectionData.FieldTower.canonicalGraphWordPath_norm_sq_le_high {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (n : ℕ) (w : Fin n → Fin 4) (q : ℕ) (hq : n + 1 ≤ q) (t : ↑(Set.Icc 0 T)) : ‖(A.canonicalGraphWordPath θ hθ n w) t‖ ^ 2 ≤ (2 / P + 2 * P) * ‖(A.realization q) t‖ ^ 2

theorem EulerAllOrderCorrectionData.FieldTower.canonicalGraphWordPath_hasDerivAt {P T : ℝ} [Fact (0 < P)] (A : FieldTower P T) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (B : FieldTower P T) (hT : 0 ≤ T) (n : ℕ) (w : Fin n → Fin 4) (q : ℕ) (hq : n + 1 ≤ q) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) (hd : HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.realization q)) ((B.realization q) ⟨t, ⋯⟩) t) : HasDerivAt (EulerVolterraConvolution.extendPath T hT (A.canonicalGraphWordPath θ hθ n w)) ((B.canonicalGraphWordPath θ hθ n w) ⟨t, ⋯⟩) t