The initial-zero primitive of an actual Bochner L² time field. In contrast to the terminal-zero primitive, this applies to the nonzero-terminal paths used in the activation argument. The factor T²/2 is proved from integration.

noncomputable def EulerInitialTimePrimitive.initialRealPrimitive {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) : E

The actual real-time primitive, normalized at the initial endpoint.

Equations

• EulerInitialTimePrimitive.initialRealPrimitive T u t = EulerTerminalTimePrimitive.realPrimitive T u t - EulerTerminalTimePrimitive.realPrimitive T u 0

theorem EulerInitialTimePrimitive.initialRealPrimitive_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) : initialRealPrimitive T u t = ∫ (s : ℝ) in 0..t, EulerTerminalTimePrimitive.zeroExtension T u s

@[simp]

theorem EulerInitialTimePrimitive.initialRealPrimitive_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) : initialRealPrimitive T u 0 = 0

theorem EulerInitialTimePrimitive.initialRealPrimitive_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) : Continuous (initialRealPrimitive T u)

theorem EulerInitialTimePrimitive.initialRealPrimitive_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) : AbsolutelyContinuousOnInterval (initialRealPrimitive T u) 0 T

theorem EulerInitialTimePrimitive.initialRealPrimitive_hasDerivAt_ae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (initialRealPrimitive T u) (↑↑u t) t

theorem EulerInitialTimePrimitive.initialRealPrimitive_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ‖initialRealPrimitive T u t‖ ^ 2 ≤ t * ‖u‖ ^ 2

The sharp pointwise initial trace estimate.

theorem EulerInitialTimePrimitive.initialRealPrimitive_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ℝ) (ht : t ∈ Set.Icc 0 T) : ‖initialRealPrimitive T u t‖ ≤ √t * ‖u‖

noncomputable def EulerInitialTimePrimitive.initialPath {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) : C(↑(Set.Icc 0 T), E)

Initial path, given by ⟨fun t => initialRealPrimitive T u t, (initialRealPrimitive_continuous T u).comp continuous_subtype_val⟩.

Equations

• EulerInitialTimePrimitive.initialPath T u = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerInitialTimePrimitive.initialRealPrimitive T u ↑t, continuous_toFun := ⋯ }

theorem EulerInitialTimePrimitive.initialPath_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u v : ↥(EulerTimeLp.TimeLp T E)) : initialPath T (u + v) = initialPath T u + initialPath T v

theorem EulerInitialTimePrimitive.initialPath_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (a : ℝ) (u : ↥(EulerTimeLp.TimeLp T E)) : initialPath T (a • u) = a • initialPath T u

theorem EulerInitialTimePrimitive.initialPath_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (_hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) : ‖initialPath T u‖ ≤ √T * ‖u‖

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

Bounded initial integration of genuine L² data.

Equations

• EulerInitialTimePrimitive.initialPrimitive T hT = { toFun := EulerInitialTimePrimitive.initialPath T, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous √T ⋯

@[simp]

theorem EulerInitialTimePrimitive.initialPrimitive_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) : ((initialPrimitive T hT) u) t = initialRealPrimitive T u ↑t

theorem EulerInitialTimePrimitive.initialPrimitive_initial {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) : ((initialPrimitive T hT) u) ⟨0, ⋯⟩ = 0

theorem EulerInitialTimePrimitive.initialPrimitive_eq_terminal_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) (t : ↑(Set.Icc 0 T)) : ((initialPrimitive T hT) u) t = ((EulerTerminalTimePrimitive.terminalPrimitive T hT) u) t - (EulerTerminalTimePrimitive.initialTrace T hT) u

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

Initial primitive time Lᵖ, given by (pathLpOperator T hT).comp (initialPrimitive T hT).

Equations

• EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT = EulerTimeLp.pathLpOperator T hT ∘SL EulerInitialTimePrimitive.initialPrimitive T hT

theorem EulerInitialTimePrimitive.initialPrimitiveTimeLp_ae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) : ↑↑((initialPrimitiveTimeLp T hT) u) =ᵐ[EulerTimeLp.timeMeasure T] initialRealPrimitive T u

theorem EulerInitialTimePrimitive.initialPrimitive_poincare {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) : ∫ (t : ℝ) in 0..T, ‖initialRealPrimitive T u t‖ ^ 2 ≤ T ^ 2 / 2 * ‖u‖ ^ 2

The sharp initial-zero Poincaré estimate is independent of the terminal value.

theorem EulerInitialTimePrimitive.initialPrimitiveTimeLp_norm_sq_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T E)) : ‖(initialPrimitiveTimeLp T hT) u‖ ^ 2 ≤ T ^ 2 / 2 * ‖u‖ ^ 2