A bounded reconstruction of genuine time-H¹ fields

The pair of L² fields (p,q) determines a continuous path by mean(p) - mean(Jq) + Jq. For an actual absolutely continuous representative of p with derivative q, this is that representative. Thus parameter derivatives and all-order bounds pass through one fixed bounded linear map.

noncomputable def EulerTimeH1Reconstruction.mean {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] E

The actual time average, expressed using the terminal primitive's initial trace.

Equations

• EulerTimeH1Reconstruction.mean T hT = (-T)⁻¹ • EulerTerminalTimePrimitive.initialTrace T hT

noncomputable def EulerTimeH1Reconstruction.valuePart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] C(↑(Set.Icc 0 T), E)

The constant part of the reconstruction.

Equations

• EulerTimeH1Reconstruction.valuePart T hT = ContinuousLinearMap.const ℝ ↑(Set.Icc 0 T) ∘SL EulerTimeH1Reconstruction.mean T hT

noncomputable def EulerTimeH1Reconstruction.derivativePart {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : ↥(EulerTimeLp.TimeLp T E) →L[ℝ] C(↑(Set.Icc 0 T), E)

The mean-zero primitive part of the reconstruction.

Equations

• EulerTimeH1Reconstruction.derivativePart T hT = EulerTerminalTimePrimitive.terminalPrimitive T hT - EulerTimeH1Reconstruction.valuePart T hT ∘SL EulerTerminalTimePrimitive.primitiveTimeLp T hT

noncomputable def EulerTimeH1Reconstruction.reconstruction {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) : ↥(EulerTimeLp.TimeLp T E) × ↥(EulerTimeLp.TimeLp T E) →L[ℝ] C(↑(Set.Icc 0 T), E)

One fixed bounded linear map from the value/derivative pair to its continuous representative.

Equations

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

theorem EulerTimeH1Reconstruction.reconstruction_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (p q : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) : ((reconstruction T hT) (p, q)) t = (mean T hT) p + (((EulerTerminalTimePrimitive.terminalPrimitive T hT) q) t - (mean T hT) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) q))

The reconstruction is the literal average plus mean-zero terminal primitive.

theorem EulerTimeH1Reconstruction.mean_constantField {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 < T) (v : E) : (mean T ⋯) (EulerTimeWeakDerivative.constantField T ⋯ v) = v

Constant fields have their actual value as time average.

theorem EulerTimeH1Reconstruction.mean_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (p : ↥(EulerTimeLp.TimeLp T E)) : ‖(mean T hT) p‖ ≤ T⁻¹ * √T * ‖p‖

The mean has the expected inverse-square-root time bound.

theorem EulerTimeH1Reconstruction.reconstruction_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 < T) (p q : ↥(EulerTimeLp.TimeLp T E)) : ‖(reconstruction T ⋯) (p, q)‖ ≤ T⁻¹ * √T * ‖p‖ + 2 * √T * ‖q‖

Uniform time evaluation is controlled by the actual L² value and derivative.

theorem EulerTimeH1Reconstruction.valuePart_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 < T) : ‖valuePart T ⋯‖ ≤ T⁻¹ * √T

The constant reconstruction component has the sharp polynomial trace cost.

theorem EulerTimeH1Reconstruction.derivativePart_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 < T) : ‖derivativePart T ⋯‖ ≤ 2 * √T

The mean-zero primitive reconstruction has only a square-root time cost.

theorem EulerTimeH1Reconstruction.reconstruction_eq_path {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 < T) (p q : ↥(EulerTimeLp.TimeLp T E)) (η : ℝ → E) (hη : AbsolutelyContinuousOnInterval η 0 T) (hp : ↑↑p =ᵐ[EulerTimeLp.timeMeasure T] η) (hq : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt η (↑↑q t) t) (t : ↑(Set.Icc 0 T)) : ((reconstruction T ⋯) (p, q)) t = η ↑t

The reconstructed path equals every genuine AC representative with the specified derivative.

theorem EulerTimeH1Reconstruction.reconstruction_contDiff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 ≤ T) (p q : P → ↥(EulerTimeLp.TimeLp T E)) {n : WithTop ℕ∞} (hp : ContDiff ℝ n p) (hq : ContDiff ℝ n q) : ContDiff ℝ n fun (x : P) => (reconstruction T hT) (p x, q x)

Smooth parameter dependence passes through the fixed H¹ reconstruction.

theorem EulerTimeH1Reconstruction.reconstruction_gevrey {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {P : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] (T : ℝ) (hT : 0 < T) (p q : P → ↥(EulerTimeLp.TimeLp T E)) (hp : ContDiff ℝ (↑⊤) p) (hq : ContDiff ℝ (↑⊤) q) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (d : ℕ) (hbp : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n p x‖ ≤ C * EulerGevrey.majorant R d n) (hbq : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n q x‖ ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => (reconstruction T ⋯) (p y, q y)) x‖ ≤ (T⁻¹ * √T * C + 2 * √T * D) * EulerGevrey.majorant R d n

Every actual parameter derivative has the uniform time-trace estimate; the trace costs a fixed polynomial multiplier, independent of the order.