Cylinder Graph Trace

Terminal Energy

theorem EulerTerminalEnergy.integral_sq_le_length_mul (g : ℝ → ℝ) {a b : ℝ} (hab : a ≤ b) (hg : ContinuousOn g (Set.Icc a b)) : (∫ (t : ℝ) in a..b, g t) ^ 2 ≤ (b - a) * ∫ (t : ℝ) in a..b, g t ^ 2

theorem EulerTerminalEnergy.norm_integral_sq_le_length_mul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (g : ℝ → E) {a b : ℝ} (hab : a ≤ b) (hg : ContinuousOn g (Set.Icc a b)) : ‖∫ (t : ℝ) in a..b, g t‖ ^ 2 ≤ (b - a) * ∫ (t : ℝ) in a..b, ‖g t‖ ^ 2

theorem EulerTerminalEnergy.terminal_trace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (η v : ℝ → E) {S t : ℝ} (ht : t ≤ S) (hv : ContinuousOn v (Set.Icc t S)) (hη : ∀ s ∈ Set.Icc t S, HasDerivAt η (v s) s) (hS : η S = 0) : ‖η t‖ ^ 2 ≤ (S - t) * ∫ (s : ℝ) in t..S, ‖v s‖ ^ 2

theorem EulerTerminalEnergy.terminal_poincare {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (η v : ℝ → E) {S : ℝ} (hS0 : 0 ≤ S) (hv : ContinuousOn v (Set.Icc 0 S)) (hη : ∀ t ∈ Set.Icc 0 S, HasDerivAt η (v t) t) (hS : η S = 0) : ∫ (t : ℝ) in 0..S, ‖η t‖ ^ 2 ≤ S ^ 2 / 2 * ∫ (t : ℝ) in 0..S, ‖v t‖ ^ 2

theorem EulerTerminalEnergy.localized_boundary_lower_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (M A R : E →L[ℝ] E) (Be Bc C₁ C₂ r L : ℝ) (hBc : 0 ≤ Bc) (hC : 0 ≤ L - Bc * C₁) (hA : ∀ (z : E), 0 ≤ inner ℝ (A z) z) (hM : ∀ (z : E), -Be * ‖z‖ ^ 2 - Bc * ‖R z‖ ^ 2 ≤ inner ℝ (M z) z) (hR : ∀ (z : E), ‖R z‖ ^ 2 ≤ C₁ * inner ℝ (A z) z + C₂ * r ^ 3 * ‖z‖ ^ 2) (z : E) : -(Be + C₂ * Bc * r ^ 3) * ‖z‖ ^ 2 ≤ inner ℝ (M z) z + L * inner ℝ (A z) z

theorem EulerTerminalEnergy.mean_form_coercive {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (η v : ℝ → E) (H : ℝ → E →L[ℝ] E) (M A : E →L[ℝ] E) (S K B L : ℝ) (hS0 : 0 ≤ S) (hK : 0 ≤ K) (hB : 0 ≤ B) (hsmall : K * S ^ 2 / 2 + B * S ≤ 1 / 2) (hv : ContinuousOn v (Set.Icc 0 S)) (hH : ContinuousOn H (Set.Icc 0 S)) (hη : ∀ t ∈ Set.Icc 0 S, HasDerivAt η (v t) t) (hS : η S = 0) (hpot : ∀ t ∈ Set.Icc 0 S, ∀ (z : E), inner ℝ ((H t) z) z ≤ K * ‖z‖ ^ 2) (hboundary : ∀ (z : E), -B * ‖z‖ ^ 2 ≤ inner ℝ (M z) z + L * inner ℝ (A z) z) : (∫ (t : ℝ) in 0..S, ‖v t‖ ^ 2) / 2 ≤ (∫ (t : ℝ) in 0..S, ‖v t‖ ^ 2 - inner ℝ ((H t) (η t)) (η t)) + inner ℝ (M (η 0)) (η 0) + L * inner ℝ (A (η 0)) (η 0)

Interval Trace

theorem EulerIntervalTrace.norm_sub_sq_le_interval_energy {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f v : ℝ → E) (a b : ℝ) (hab : a ≤ b) (hv : ContinuousOn v (Set.Icc a b)) (hf : ∀ t ∈ Set.Icc a b, HasDerivAt f (v t) t) (s t : ℝ) (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) : ‖f t - f s‖ ^ 2 ≤ (b - a) * ∫ (r : ℝ) in a..b, ‖v r‖ ^ 2

theorem EulerIntervalTrace.pointwise_H1_trace {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (f v : ℝ → E) (a b : ℝ) (hab : a < b) (hv : ContinuousOn v (Set.Icc a b)) (hf : ∀ t ∈ Set.Icc a b, HasDerivAt f (v t) t) (t : ℝ) (ht : t ∈ Set.Icc a b) : ‖f t‖ ^ 2 ≤ (2 / (b - a) * ∫ (s : ℝ) in a..b, ‖f s‖ ^ 2) + 2 * (b - a) * ∫ (s : ℝ) in a..b, ‖v s‖ ^ 2

Point evaluation on an interval is bounded by the actual zeroth and first derivative energies.

theorem EulerCylinderGraphTrace.angular_hasDerivAt (period : ℝ) {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.Vector3) (t : ℝ) : HasDerivAt (fun (s : ℝ) => f (x, ↑s)) (EulerTransportDerivatives.fieldDerivative period (0, 1) f (x, ↑t)) t

theorem EulerCylinderGraphTrace.cylinder_pointwise_trace (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (x : EulerLiftedGradientSpace.Vector3) (θ : AddCircle period) : ‖f (x, θ)‖ ^ 2 ≤ (2 / period * ∫ (s : AddCircle period), ‖f (x, s)‖ ^ 2) + 2 * period * ∫ (s : AddCircle period), ‖EulerTransportDerivatives.fieldDerivative period (0, 1) f (x, s)‖ ^ 2

Point evaluation in the periodic coordinate costs one angular derivative, with a bound independent of the chosen phase.

theorem EulerCylinderGraphTrace.graph_memLp_and_energy_bound (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (f : EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hfL2 : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period)) (hdL2 : MeasureTheory.MemLp (EulerTransportDerivatives.fieldDerivative period (0, 1) f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle period) (hθ : Continuous θ) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.Vector3) => f (x, θ x)) 2 MeasureTheory.volume ∧ ∫ (x : EulerLiftedGradientSpace.Vector3), ‖f (x, θ x)‖ ^ 2 ≤ 2 / period * ∫ (z : EulerLiftedGradientSpace.LiftDomain period), ‖f z‖ ^ 2 ∂EulerLiftedGradientSpace.liftMeasure period + 2 * period * ∫ (z : EulerLiftedGradientSpace.LiftDomain period), ‖EulerTransportDerivatives.fieldDerivative period (0, 1) f z‖ ^ 2 ∂EulerLiftedGradientSpace.liftMeasure period

Pullback to any continuous phase graph preserves square integrability. The estimate has no dependence on the phase frequency.