Source (26) for the actual stationary transverse solution. The endpoint matrix is the constructed Dirichlet-to-Neumann operator and its norm is derived from the explicit moving-projection trial. The selected velocity is the genuine derivative η_t minus Mη, not a separately prescribed matrix output.

An explicit terminal-layer H¹ trial obtained by multiplying a differentiable projection path by the smooth exponential ramp. Both energy estimates concern the actual Bochner L² derivative and primitive.

An explicit smooth terminal-layer trial profile. Its endpoint values are zero and one, and its squared value/derivative integrals are at most 2/L and 2*L when L*T ≥ 1. These are the same energy bounds needed for the piecewise linear terminal ramp in the activation argument.

noncomputable def EulerTerminalLayerRamp.ramp (T L t : ℝ) : ℝ

Ramp, given by (Real.exp (L * (t - T)) - Real.exp (-L * T)) / (1 - Real.exp (-L * T)).

Equations

• EulerTerminalLayerRamp.ramp T L t = (Real.exp (L * (t - T)) - Real.exp (-L * T)) / (1 - Real.exp (-L * T))

noncomputable def EulerTerminalLayerRamp.rampDerivative (T L t : ℝ) : ℝ

Ramp derivative, given by L * Real.exp (L * (t - T)) / (1 - Real.exp (-L * T)).

Equations

• EulerTerminalLayerRamp.rampDerivative T L t = L * Real.exp (L * (t - T)) / (1 - Real.exp (-L * T))

theorem EulerTerminalLayerRamp.denominator_lower {T L : ℝ} (hLT : 1 ≤ L * T) : 1 / 2 ≤ 1 - Real.exp (-L * T)

theorem EulerTerminalLayerRamp.denominator_pos {T L : ℝ} (hLT : 1 ≤ L * T) : 0 < 1 - Real.exp (-L * T)

@[simp]

theorem EulerTerminalLayerRamp.ramp_initial (T L : ℝ) : ramp T L 0 = 0

theorem EulerTerminalLayerRamp.ramp_terminal {T L : ℝ} (hLT : 1 ≤ L * T) : ramp T L T = 1

theorem EulerTerminalLayerRamp.ramp_hasDerivAt (T L t : ℝ) : HasDerivAt (ramp T L) (rampDerivative T L t) t

theorem EulerTerminalLayerRamp.ramp_continuous (T L : ℝ) : Continuous (ramp T L)

theorem EulerTerminalLayerRamp.rampDerivative_continuous (T L : ℝ) : Continuous (rampDerivative T L)

theorem EulerTerminalLayerRamp.ramp_nonneg {T L t : ℝ} (hL : 0 ≤ L) (hLT : 1 ≤ L * T) (ht : 0 ≤ t) : 0 ≤ ramp T L t

theorem EulerTerminalLayerRamp.ramp_le_exp {T L t : ℝ} (hLT : 1 ≤ L * T) : ramp T L t ≤ 2 * Real.exp (L * (t - T))

theorem EulerTerminalLayerRamp.rampDerivative_nonneg {T L t : ℝ} (hL : 0 ≤ L) (hLT : 1 ≤ L * T) : 0 ≤ rampDerivative T L t

theorem EulerTerminalLayerRamp.rampDerivative_le_exp {T L t : ℝ} (hL : 0 ≤ L) (hLT : 1 ≤ L * T) : rampDerivative T L t ≤ 2 * L * Real.exp (L * (t - T))

theorem EulerTerminalLayerRamp.ramp_sq_le {T L t : ℝ} (hL : 0 ≤ L) (hLT : 1 ≤ L * T) (ht : 0 ≤ t) : ramp T L t ^ 2 ≤ 4 * Real.exp (2 * L * (t - T))

theorem EulerTerminalLayerRamp.rampDerivative_sq_le {T L t : ℝ} (hL : 0 ≤ L) (hLT : 1 ≤ L * T) : rampDerivative T L t ^ 2 ≤ 4 * L ^ 2 * Real.exp (2 * L * (t - T))

theorem EulerTerminalLayerRamp.exp_kernel_integral_le {T L : ℝ} (hL : 0 < L) : ∫ (t : ℝ) in 0..T, Real.exp (2 * L * (t - T)) ≤ 1 / (2 * L)

theorem EulerTerminalLayerRamp.ramp_energy {T L : ℝ} (hT : 0 ≤ T) (hL : 0 < L) (hLT : 1 ≤ L * T) : ∫ (t : ℝ) in 0..T, ramp T L t ^ 2 ≤ 2 / L

theorem EulerTerminalLayerRamp.rampDerivative_energy {T L : ℝ} (hT : 0 ≤ T) (hL : 0 < L) (hLT : 1 ≤ L * T) : ∫ (t : ℝ) in 0..T, rampDerivative T L t ^ 2 ≤ 2 * L

@[instance_reducible]

noncomputable def EulerTerminalProjectionTrial.instTerminalProjectionTrial1 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] E)

Cache the standard NormedAddCommGroup (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTerminalProjectionTrial.instTerminalProjectionTrial1 = inferInstance

@[instance_reducible]

noncomputable def EulerTerminalProjectionTrial.instTerminalProjectionTrial2 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] E)

Cache the standard NormedSpace ℝ (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTerminalProjectionTrial.instTerminalProjectionTrial2 = inferInstance

@[instance_reducible]

noncomputable def EulerTerminalProjectionTrial.instTerminalProjectionTrial3 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] : AddCommGroup (U →L[ℝ] E)

Cache the standard AddCommGroup (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTerminalProjectionTrial.instTerminalProjectionTrial3 = inferInstance.toAddCommGroup

@[instance_reducible]

noncomputable def EulerTerminalProjectionTrial.instTerminalProjectionTrial4 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] : Module ℝ (U →L[ℝ] E)

Cache the standard Module ℝ (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTerminalProjectionTrial.instTerminalProjectionTrial4 = inferInstance.toModule

@[instance_reducible]

noncomputable def EulerTerminalProjectionTrial.instTerminalProjectionTrial5 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] : TopologicalSpace (U →L[ℝ] E)

Cache the standard TopologicalSpace (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTerminalProjectionTrial.instTerminalProjectionTrial5 = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

noncomputable def EulerTerminalProjectionTrial.operatorEvaluation {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (A : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : U →L[ℝ] C(↑(Set.Icc 0 T), E)

Evaluation of an actual continuous operator path as a bounded map into paths.

Equations

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

@[simp]

theorem EulerTerminalProjectionTrial.operatorEvaluation_apply {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (A : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (Y : U) (t : ↑(Set.Icc 0 T)) : ((operatorEvaluation T A) Y) t = (A t) Y

noncomputable def EulerTerminalProjectionTrial.trialFrame {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T L : ℝ) (P : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Trial frame, given by ⟨fun t => ramp T L t • P t, ((ramp_continuous T L).comp continuous_subtype_val).smul P.continuous⟩.

Equations

• EulerTerminalProjectionTrial.trialFrame T L P = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerTerminalLayerRamp.ramp T L ↑t • P t, continuous_toFun := ⋯ }

noncomputable def EulerTerminalProjectionTrial.trialFrameDerivative {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Trial frame derivative as an element of C(Icc (0 : ℝ) T, U →L[ℝ] E).

Equations

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

noncomputable def EulerTerminalProjectionTrial.trialDerivative {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

Trial derivative, given by (pathLpOperator T hT).comp (operatorEvaluation T (trialFrameDerivative T L P P₁)).

Equations

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

theorem EulerTerminalProjectionTrial.trialFrame_hasDerivWithinAt {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT P) (P₁ t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (trialFrame T L P)) ((trialFrameDerivative T L P P₁) t) (Set.Icc 0 T) ↑t

theorem EulerTerminalProjectionTrial.trialDerivative_realizes {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT P) (P₁ t) (Set.Icc 0 T) ↑t) (Y : U) : ∀ᵐ (t : ℝ) ∂EulerTimeLp.timeMeasure T, HasDerivAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath T hT (trialFrame T L P) s) Y) (↑↑((trialDerivative T hT L P P₁) Y) t) t

The trial derivative is the actual derivative of its explicit ramp-times-projection path.

theorem EulerTerminalProjectionTrial.initialPrimitive_trialDerivative {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT P) (P₁ t) (Set.Icc 0 T) ↑t) (Y : U) (t : ↑(Set.Icc 0 T)) : ((EulerInitialTimePrimitive.initialPrimitive T hT) ((trialDerivative T hT L P P₁) Y)) t = EulerTerminalLayerRamp.ramp T L ↑t • (P t) Y

Integrating the constructed L² derivative gives the prescribed trial at every time.

theorem EulerTerminalProjectionTrial.initialPrimitiveTimeLp_trialDerivative {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT P) (P₁ t) (Set.Icc 0 T) ↑t) (Y : U) : (EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) ((trialDerivative T hT L P P₁) Y) = EulerTimeLp.pathLp T hT ((operatorEvaluation T (trialFrame T L P)) Y)

theorem EulerTerminalProjectionTrial.norm_add_sq_le {E : Type u_1} [NormedAddCommGroup E] (a b : E) : ‖a + b‖ ^ 2 ≤ 2 * ‖a‖ ^ 2 + 2 * ‖b‖ ^ 2

theorem EulerTerminalProjectionTrial.trialFrameDerivative_apply_sq_le {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (M : ℝ) (_hM : 0 ≤ M) (hP : ∀ (t : ↑(Set.Icc 0 T)), ‖P t‖ ≤ 1) (hP₁ : ∀ (t : ↑(Set.Icc 0 T)), ‖P₁ t‖ ≤ M) (Y : U) (t : ↑(Set.Icc 0 T)) : ‖((trialFrameDerivative T L P P₁) t) Y‖ ^ 2 ≤ (2 * EulerTerminalLayerRamp.rampDerivative T L ↑t ^ 2 + 2 * EulerTerminalLayerRamp.ramp T L ↑t ^ 2 * M ^ 2) * ‖Y‖ ^ 2

theorem EulerTerminalProjectionTrial.trialDerivative_norm_sq_le {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hL : 0 < L) (hLT : 1 ≤ L * T) (M : ℝ) (hM : 0 ≤ M) (hP : ∀ (t : ↑(Set.Icc 0 T)), ‖P t‖ ≤ 1) (hP₁ : ∀ (t : ↑(Set.Icc 0 T)), ‖P₁ t‖ ≤ M) (Y : U) : ‖(trialDerivative T hT L P P₁) Y‖ ^ 2 ≤ (4 * L + 4 * M ^ 2 / L) * ‖Y‖ ^ 2

The actual L² derivative cost of the explicit terminal-layer trial.

theorem EulerTerminalProjectionTrial.trialDisplacement_norm_sq_le {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup U] [NormedSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (L : ℝ) (P P₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT P) (P₁ t) (Set.Icc 0 T) ↑t) (hL : 0 < L) (hLT : 1 ≤ L * T) (hP : ∀ (t : ↑(Set.Icc 0 T)), ‖P t‖ ≤ 1) (Y : U) : ‖(EulerInitialTimePrimitive.initialPrimitiveTimeLp T hT) ((trialDerivative T hT L P P₁) Y)‖ ^ 2 ≤ 2 / L * ‖Y‖ ^ 2

The corresponding physical displacement cost retains the inverse layer width.

The explicit activation trial and its endpoint-energy bound. The trial uses the actual moving normal, not a deformation-frame condition number. A layer of width 1/h gives ‖Λ‖ ≤ (4 + 64 CM² + 2 CH) h under the source's low history bounds.

The actual orthogonal projection onto a moving ray's perpendicular plane. The derivative bound depends on the ray equation through ‖m'‖/‖m‖, and therefore costs only the parent matrix norm, with no deformation-gradient loss.

@[instance_reducible]

noncomputable def EulerMovingNormalProjection.instMovingNormalProjection1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] E)

Cache the standard NormedAddCommGroup (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerMovingNormalProjection.instMovingNormalProjection1 = inferInstance

@[instance_reducible]

noncomputable def EulerMovingNormalProjection.instMovingNormalProjection2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] E)

Cache the standard NormedSpace ℝ (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerMovingNormalProjection.instMovingNormalProjection2 = inferInstance

@[instance_reducible]

noncomputable def EulerMovingNormalProjection.instMovingNormalProjection3 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : AddCommGroup (E →L[ℝ] E)

Cache the standard AddCommGroup (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerMovingNormalProjection.instMovingNormalProjection3 = inferInstance.toAddCommGroup

@[instance_reducible]

noncomputable def EulerMovingNormalProjection.instMovingNormalProjection4 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Module ℝ (E →L[ℝ] E)

Cache the standard Module ℝ (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerMovingNormalProjection.instMovingNormalProjection4 = inferInstance.toModule

@[instance_reducible]

noncomputable def EulerMovingNormalProjection.instMovingNormalProjection5 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : TopologicalSpace (E →L[ℝ] E)

Cache the standard TopologicalSpace (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerMovingNormalProjection.instMovingNormalProjection5 = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

noncomputable def EulerMovingNormalProjection.normalProjection {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : E) : E →L[ℝ] E

Normal projection, given by ContinuousLinearMap.id ℝ E - (‖m‖ ^ 2)⁻¹ • rankOne ℝ m m.

Equations

• EulerMovingNormalProjection.normalProjection m = ContinuousLinearMap.id ℝ E - (‖m‖ ^ 2)⁻¹ • ((InnerProductSpace.rankOne ℝ) m) m

theorem EulerMovingNormalProjection.normalProjection_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m x : E) : (normalProjection m) x = x - (inner ℝ m x / ‖m‖ ^ 2) • m

theorem EulerMovingNormalProjection.normalProjection_tangent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : E) (hm : m ≠ 0) (x : E) : inner ℝ m ((normalProjection m) x) = 0

theorem EulerMovingNormalProjection.normalProjection_fixed {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m x : E) (hx : inner ℝ m x = 0) : (normalProjection m) x = x

theorem EulerMovingNormalProjection.normalProjection_norm_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : E) (hm : m ≠ 0) (x : E) : ‖(normalProjection m) x‖ ^ 2 = ‖x‖ ^ 2 - inner ℝ m x ^ 2 / ‖m‖ ^ 2

theorem EulerMovingNormalProjection.normalProjection_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m : E) (hm : m ≠ 0) : ‖normalProjection m‖ ≤ 1

noncomputable def EulerMovingNormalProjection.normalProjectionDerivative {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m m₁ : E) : E →L[ℝ] E

Normal projection derivative, given by -((- (2 * ⟪m, m₁⟫_ℝ) / (‖m‖ ^ 2) ^ 2) • rankOne ℝ m m + (‖m‖ ^ 2)⁻¹ • (rankOne ℝ m₁ m + rankOne ℝ m m₁)).

Equations

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

theorem EulerMovingNormalProjection.normalProjection_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {m : ℝ → E} {m₁ : E} {t : ℝ} (hd : HasDerivAt m m₁ t) (hm : m t ≠ 0) : HasDerivAt (fun (s : ℝ) => normalProjection (m s)) (normalProjectionDerivative (m t) m₁) t

The projection derivative is derived from the actual ray derivative.

theorem EulerMovingNormalProjection.normalProjection_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {m : ℝ → E} {m₁ : E} {t : ℝ} {S : Set ℝ} (hd : HasDerivWithinAt m m₁ S t) (hm : m t ≠ 0) : HasDerivWithinAt (fun (s : ℝ) => normalProjection (m s)) (normalProjectionDerivative (m t) m₁) S t

theorem EulerMovingNormalProjection.normalProjection_continuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {f : α → E} (hf : Continuous f) (hne : ∀ (a : α), f a ≠ 0) : Continuous fun (a : α) => normalProjection (f a)

theorem EulerMovingNormalProjection.normalProjectionDerivative_continuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {α : Type u_2} [TopologicalSpace α] {f g : α → E} (hf : Continuous f) (hg : Continuous g) (hne : ∀ (a : α), f a ≠ 0) : Continuous fun (a : α) => normalProjectionDerivative (f a) (g a)

theorem EulerMovingNormalProjection.normalProjectionDerivative_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m m₁ : E) (hm : m ≠ 0) : ‖normalProjectionDerivative m m₁‖ ≤ 4 * ‖m₁‖ / ‖m‖

The bound is independent of the length of the ray.

theorem EulerMovingNormalProjection.normalProjectionDerivative_ray_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (m : E) (hm : m ≠ 0) (M : E →L[ℝ] E) : ‖normalProjectionDerivative m (-(ContinuousLinearMap.adjoint M) m)‖ ≤ 4 * ‖M‖

For the actual ray equation m'=-M* m, only the parent gradient norm enters.

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedAddCommGroup (E →L[ℝ] E)

Cache the standard NormedAddCommGroup (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : NormedSpace ℝ (E →L[ℝ] E)

Cache the standard NormedSpace ℝ (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial2 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial3 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : AddCommGroup (E →L[ℝ] E)

Cache the standard AddCommGroup (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial3 = inferInstance.toAddCommGroup

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial4 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Module ℝ (E →L[ℝ] E)

Cache the standard Module ℝ (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial4 = inferInstance.toModule

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial5 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : TopologicalSpace (E →L[ℝ] E)

Cache the standard TopologicalSpace (E →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial5 = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial6 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedAddCommGroup (U →L[ℝ] E)

Cache the standard NormedAddCommGroup (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial6 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial7 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ (U →L[ℝ] E)

Cache the standard NormedSpace ℝ (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial7 = inferInstance

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial8 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : AddCommGroup (U →L[ℝ] E)

Cache the standard AddCommGroup (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial8 = inferInstance.toAddCommGroup

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial9 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : Module ℝ (U →L[ℝ] E)

Cache the standard Module ℝ (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial9 = inferInstance.toModule

@[instance_reducible]

noncomputable def EulerTransverseActivationTrial.instTransverseActivationTrial10 {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] : TopologicalSpace (U →L[ℝ] E)

Cache the standard TopologicalSpace (U →L[ℝ] E) instance to shorten typeclass synthesis.

Equations

• EulerTransverseActivationTrial.instTransverseActivationTrial10 = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

noncomputable def EulerTransverseActivationTrial.projectionPath {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (m : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Projection path, given by ⟨fun t => (normalProjection (m t)).comp R, (normalProjection_continuous m.continuous hne).clm_comp continuous_const⟩.

Equations

• EulerTransverseActivationTrial.projectionPath T m hne R = { toFun := fun (t : ↑(Set.Icc 0 T)) => EulerMovingNormalProjection.normalProjection (m t) ∘SL R, continuous_toFun := ⋯ }

noncomputable def EulerTransverseActivationTrial.projectionDerivativePath {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) : C(↑(Set.Icc 0 T), U →L[ℝ] E)

Projection derivative path as an element of C(Icc (0 : ℝ) T, U →L[ℝ] E).

Equations

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

theorem EulerTransverseActivationTrial.projectionPath_hasDerivWithinAt {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT m) (m₁ t) (Set.Icc 0 T) ↑t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (projectionPath T m hne R)) ((projectionDerivativePath T m m₁ hne R) t) (Set.Icc 0 T) ↑t

theorem EulerTransverseActivationTrial.projectionPath_norm_le {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (m : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) (hR : ‖R‖ ≤ 1) (t : ↑(Set.Icc 0 T)) : ‖(projectionPath T m hne R) t‖ ≤ 1

theorem EulerTransverseActivationTrial.projectionDerivativePath_norm_le {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) [CompleteSpace E] (hR : ‖R‖ ≤ 1) (M : ↑(Set.Icc 0 T) → E →L[ℝ] E) (hRay : ∀ (t : ↑(Set.Icc 0 T)), m₁ t = -(ContinuousLinearMap.adjoint (M t)) (m t)) (B : ℝ) (_hB : 0 ≤ B) (hM : ∀ (t : ↑(Set.Icc 0 T)), ‖M t‖ ≤ B) (t : ↑(Set.Icc 0 T)) : ‖(projectionDerivativePath T m m₁ hne R) t‖ ≤ 4 * B

noncomputable def EulerTransverseActivationTrial.activationTrial {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) (h : ℝ) : U →L[ℝ] ↥(EulerTimeLp.TimeLp T E)

The actual derivative of the explicit terminal-layer displacement.

Equations

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

theorem EulerTransverseActivationTrial.activationTrial_primitive {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT m) (m₁ t) (Set.Icc 0 T) ↑t) [CompleteSpace E] (h : ℝ) (Y : U) (t : ↑(Set.Icc 0 T)) : ((EulerInitialTimePrimitive.initialPrimitive T hT) ((activationTrial T hT m m₁ hne R h) Y)) t = EulerTerminalLayerRamp.ramp T h ↑t • (EulerMovingNormalProjection.normalProjection (m t)) (R Y)

theorem EulerTransverseActivationTrial.activationTrial_tangent {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT m) (m₁ t) (Set.Icc 0 T) ↑t) [CompleteSpace E] (h : ℝ) (Y : U) (t : ↑(Set.Icc 0 T)) : inner ℝ (m t) (((EulerInitialTimePrimitive.initialPrimitive T hT) ((activationTrial T hT m m₁ hne R h) Y)) t) = 0

theorem EulerTransverseActivationTrial.activationTrial_terminal {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT m) (m₁ t) (Set.Icc 0 T) ↑t) [CompleteSpace E] (h : ℝ) (hLayer : 1 ≤ h * T) (hR : ∀ (Y : U), inner ℝ (m ⟨T, ⋯⟩) (R Y) = 0) (Y : U) : ((EulerInitialTimePrimitive.initialPrimitive T hT) ((activationTrial T hT m m₁ hne R h) Y)) ⟨T, ⋯⟩ = R Y

theorem EulerTransverseActivationTrial.potential_abs_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) (hT : 0 ≤ T) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (u : ↥(EulerTimeLp.TimeLp T E)) : |inner ℝ ((EulerTimeLp.timeMultiplier T hT H) u) u| ≤ ‖H‖ * ‖u‖ ^ 2

theorem EulerTransverseActivationTrial.activation_endpoint_norm {E : Type u_1} {U : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup U] [InnerProductSpace ℝ U] (T : ℝ) (hT : 0 ≤ T) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (R : U →L[ℝ] E) (hd : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT m) (m₁ t) (Set.Icc 0 T) ↑t) [CompleteSpace E] [CompleteSpace U] (h : ℝ) (hh : 0 < h) (hLayer : 1 ≤ h * T) (hR : ‖R‖ ≤ 1) (CM CH : ℝ) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (M : ↑(Set.Icc 0 T) → E →L[ℝ] E) (hRay : ∀ (t : ↑(Set.Icc 0 T)), m₁ t = -(ContinuousLinearMap.adjoint (M t)) (m t)) (hM : ∀ (t : ↑(Set.Icc 0 T)), ‖M t‖ ≤ CM * h) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hHs : ∀ (t : ↑(Set.Icc 0 T)), (↑(H t)).IsSymmetric) (hHnorm : ‖H‖ ≤ CH * h ^ 2) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) : ‖EulerTransverseEndpointEnergy.dirichletToNeumann T hT (fun (t : ↑(Set.Icc 0 T)) => m t) H K hK hH hsmall (activationTrial T hT m m₁ hne R h)‖ ≤ (4 + 64 * CM ^ 2 + 2 * CH) * h

All input bounds concern the parent coefficients and the actual ray. The endpoint operator and its O(h) norm are constructed conclusions.

def EulerTransverseActivationSelection.activationConstant (CM CH : ℝ) : ℝ

Activation constant, given by 4 + 64 * CM ^ 2 + 2 * CH.

Equations

• EulerTransverseActivationSelection.activationConstant CM CH = 4 + 64 * CM ^ 2 + 2 * CH

noncomputable def EulerTransverseActivationSelection.terminalPerturbation {E : Type u_2} {V : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 ≤ T) (R : V →ₗᵢ[ℝ] E) (M : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (p q : V) (h : ℝ) : V →L[ℝ] V

The actual terminal matrix after subtracting the prescribed shear.

Equations

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

theorem EulerTransverseActivationSelection.corrected_velocity_tangent {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (T : ℝ) (hT : 0 < T) (m m₁ : C(↑(Set.Icc 0 T), E)) (M : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hdm : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ m) (m₁ t) (Set.Icc 0 T) ↑t) (hRay : ∀ (t : ↑(Set.Icc 0 T)), m₁ t = -(ContinuousLinearMap.adjoint (M t)) (m t)) (η v : ℝ → E) (hdη : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt η (v ↑t) (Set.Icc 0 T) ↑t) (htan : ∀ (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (η ↑t) = 0) (t : ↑(Set.Icc 0 T)) : inner ℝ (m t) (v ↑t - (M t) (η ↑t)) = 0

Differentiating the actual moving tangency constraint makes η_t−Mη tangent.

theorem EulerTransverseActivationSelection.select_actual_activation {U : Type u_1} {E : Type u_2} {V : Type u_3} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (T : ℝ) (hT : 0 < T) (Q Q₁ : C(↑(Set.Icc 0 T), U →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (x : U), c * ‖x‖ ^ 2 ≤ ‖(Q t) x‖ ^ 2) (hdQ : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ Q) (Q₁ t) (Set.Icc 0 T) ↑t) (m m₁ : C(↑(Set.Icc 0 T), E)) (hne : ∀ (t : ↑(Set.Icc 0 T)), m t ≠ 0) (hdm : ∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T ⋯ m) (m₁ t) (Set.Icc 0 T) ↑t) (hm : ∀ (t : ↑(Set.Icc 0 T)) (x : U), inner ℝ (m t) ((Q t) x) = 0) (hRange : ∀ (t : ↑(Set.Icc 0 T)) (η : E), inner ℝ (m t) η = 0 → ∃ (x : U), (Q t) x = η) (R : V →ₗᵢ[ℝ] E) (hR : ∀ (Y : V), inner ℝ (m ⟨T, ⋯⟩) (R Y) = 0) (H : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hHs : ∀ (t : ↑(Set.Icc 0 T)), (↑(H t)).IsSymmetric) (K : ℝ) (hK : 0 ≤ K) (hH : ∀ (t : ↑(Set.Icc 0 T)) (x : E), inner ℝ ((H t) x) x ≤ K * ‖x‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (M : C(↑(Set.Icc 0 T), E →L[ℝ] E)) (hRay : ∀ (t : ↑(Set.Icc 0 T)), m₁ t = -(ContinuousLinearMap.adjoint (M t)) (m t)) (h CM CH ε : ℝ) (hh : 0 < h) (hLayer : 1 ≤ h * T) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hε : 0 ≤ ε) (hM : ∀ (t : ↑(Set.Icc 0 T)), ‖M t‖ ≤ CM * h) (hHnorm : ‖H‖ ≤ CH * h ^ 2) (p q : V) (hp : ‖p‖ = 1) (hq : ‖q‖ = 1) (hpq : inner ℝ p q = 0) (hεsmall : 16 * (activationConstant CM CH + 1) * ε ≤ 1) (hB : ‖terminalPerturbation T ⋯ R M p q h‖ ≤ ε * h) (hBpp : inner ℝ ((terminalPerturbation T ⋯ R M p q h) p) p < 0) : ∃ (Y : V), have L := EulerTransverseActivationTrial.activationTrial T ⋯ m m₁ hne R.toContinuousLinearMap h; have u := (EulerTransverseEndpointEnergy.endpointDerivative T ⋯ (fun (t : ↑(Set.Icc 0 T)) => m t) H K hK hH hsmall L) Y; have η := EulerInitialTimePrimitive.initialRealPrimitive T u; have v := EulerTransverseEndpointVelocity.physicalVelocityPath T ⋯ Q Q₁ c hc hQ H u; have w := fun (t : ℝ) => v t - (EulerVolterraConvolution.extendPath T ⋯ M t) (η t); η 0 = 0 ∧ η T = R Y ∧ Continuous v ∧ (∀ (t : ↑(Set.Icc 0 T)), HasDerivWithinAt η (v ↑t) (Set.Icc 0 T) ↑t) ∧ (∀ (t : ↑(Set.Icc 0 T)), inner ℝ (m t) (w ↑t) = 0) ∧ inner ℝ (w T) (R q) = 1 ∧ -8 * (activationConstant CM CH + 1) ≤ inner ℝ (w T) (R p) ∧ inner ℝ (w T) (R p) ≤ 0 ∧ ‖Y‖ ≤ 8 * (activationConstant CM CH + 1) / h

The activation choice is attached to the actual weak inverse, its continuous physical derivative, and the derived endpoint energy bound.