The terminal primitive of a genuine Bochner L² time field #
The derivative is the input equivalence class. Integration of its zero extension constructs the continuous representative, its zero terminal trace, and its almost-everywhere derivative. No primitive or evolution solution is assumed.
The canonical time representative extended by zero outside the time interval.
Equations
- EulerTerminalTimePrimitive.zeroExtension T u = (Set.Icc 0 T).indicator ↑↑u
Instances For
Zero extension preserves genuine square integrability.
The finite time interval makes the zero extension Bochner integrable.
The zero extension is the original time field almost everywhere on its interval.
The actual real-valued-time representative, with terminal value zero.
Equations
- EulerTerminalTimePrimitive.realPrimitive T u t = ∫ (s : ℝ) in T..t, EulerTerminalTimePrimitive.zeroExtension T u s
Instances For
The constructed primitive is continuous on all of real time.
The terminal condition holds by construction.
All increments are the literal Bochner integrals of the zero-extended derivative.
On the time interval this is exactly the terminal integral of the input field.
The constructed real-time representative has its genuine derivative almost everywhere.
Its derivative on the time interval is the original Bochner L² field.
The genuine continuous path on the prescribed time interval.
Equations
- EulerTerminalTimePrimitive.primitivePath T u = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerTerminalTimePrimitive.realPrimitive T u ↑t, continuous_toFun := ⋯ }
Instances For
Cauchy--Schwarz for a square-integrable scalar function on an interval.
Bochner Cauchy--Schwarz, requiring actual square integrability rather than continuity.
The squared norm of the zero extension is integrable on all of real time.
Zero extension preserves the literal L² time energy.
The sharp terminal trace bound at every time, with the global derivative energy.
The pointwise square-root form of the sharp terminal trace estimate.
The constructed representative is absolutely continuous, also for vector-valued inputs.
The zero extension respects addition as an actual Lebesgue almost-everywhere identity.
The zero extension respects real scalar multiplication almost everywhere.
The primitive path respects addition of genuine L² equivalence classes.
The primitive path respects real scalar multiplication.
The continuous-path norm is bounded by the sharp terminal trace constant.
Bounded terminal integration from actual Bochner L² fields to continuous paths.
Equations
- EulerTerminalTimePrimitive.terminalPrimitive T hT = { toFun := EulerTerminalTimePrimitive.primitivePath T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous √T ⋯
Instances For
Evaluation is the actual integral representative.
The bounded primitive has exactly zero terminal trace.
The sharp pointwise squared trace estimate for the bounded primitive.
Evaluation at any interval point is a continuous linear map of the derivative.
Equations
Instances For
The initial trace, with its zero-terminal normalization.
Equations
Instances For
The bounded primitive regarded as an actual Bochner L² time field.
Equations
Instances For
The Bochner primitive is represented by the same continuous real-time function.
The primitive's increments within the interval are literal integrals of its L² derivative.
The explicit initial trace is the negative total integral of the derivative.
The initial trace has the exact squared energy estimate from the source.
The operator norm of terminal integration is bounded by the square root of the interval length.
Evaluation retains the sharper bound corresponding to the remaining interval length.
The initial trace is a bounded map with the exact source trace constant.
The integral version of the terminal Poincaré estimate, for actual L² derivative data.
The sharp source Poincaré constant for the genuine bounded Bochner primitive.
The corresponding operator norm bound, suitable for composing variational forms.
Distinct derivative classes give distinct terminal-zero paths. Thus Bochner L², equipped with the derivative norm, is a faithful Hilbert model of these terminal H¹ paths when the target is a Hilbert space.
Every absolutely continuous terminal-zero path with the prescribed L² derivative is the constructed primitive. This identifies arbitrary genuine H¹ test paths with the derivative-coordinate model used by the variational form.