A fully constructed normal and terminal coordinate for a positive activation time. The initial matching statements concern the actual source history and its continuation, with no normal-choice premise.
theorem
EulerPacketActivationHistory.activation_cross_ne_zero
(m v : EulerSmoothLimit.Space)
(hm : m ≠ 0)
(hv : v ≠ 0)
(hmv : inner ℝ m v = 0)
:
noncomputable def
EulerPacketActivationHistory.activatedData
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(m v : ℝ → EulerSmoothLimit.Space)
(hm : m τ ≠ 0)
(hv : v τ ≠ 0)
(hmv : inner ℝ (m τ) (v τ) = 0)
:
Activated data, given by D.activation ⟨τ,hτ.le,hτT.le⟩ (cross (unit (m τ)) (unit (v τ))) (activation_cross_ne_zero _ _ hm hv hmv).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketActivationHistory.activatedHistory
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(m v : ℝ → EulerSmoothLimit.Space)
(hm : m τ ≠ 0)
(hv : v τ ≠ 0)
(hmv : inner ℝ (m τ) (v τ) = 0)
:
EulerTransversePacketProvider.HistoryData ((activatedData D τ hτ hτT m v hm hv hmv).initial τ hτ ⋯)
Activated history, constructed using B.reframe.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketActivationHistory.constructed_initial_matching
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(m v : ℝ → EulerSmoothLimit.Space)
(hm : m τ ≠ 0)
(hv : v τ ≠ 0)
(hmv : inner ℝ (m τ) (v τ) = 0)
(hHs : ∀ (t : ↑(Set.Icc 0 (D.initial τ hτ ⋯).T)), (↑((B.H.field t) 0)).IsSymmetric)
(h CM CH ζ a ε : ℝ)
(hh : 0 < h)
(hLayer : 1 ≤ h * τ)
(hCM : 0 ≤ CM)
(hCH : 0 ≤ CH)
(hζ : 0 ≤ ζ)
(hε : 0 < ε)
(hM : ∀ (t : ↑(Set.Icc 0 τ)), ‖((D.initial τ hτ ⋯).M.field t) 0‖ ≤ CM * h)
(hHnorm : ‖B.coefficients.labelHessian 0‖ ≤ CH * h ^ 2)
(hζsmall : 16 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * ζ ≤ 1)
(hB :
‖(D.M.field ⟨τ, ⋯⟩) 0 - h • ((InnerProductSpace.rankOne ℝ) (EulerPacketNormalizedPrimary.unit (v τ)))
(EulerPacketNormalizedPrimary.unit (m τ))‖ ≤ ζ * h)
(hBpp :
inner ℝ (((D.M.field ⟨τ, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit (m τ))) (EulerPacketNormalizedPrimary.unit (m τ)) < 0)
:
let Da := activatedData D τ hτ hτT m v hm hv hmv;
have Ba := activatedHistory D τ hτ hτT B m v hm hv hmv;
have s₀ :=
EulerPacketMovingFrame.activationRayScale (D.deformationEquiv ⟨τ, ⋯⟩ 0)
(EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (m τ)) (EulerPacketNormalizedPrimary.unit (v τ)));
0 < s₀ ∧ EulerPacketMovingFrame.scaledRay m v (fun (s : ℝ) => (Da.normal.field (Da.clamp s)) 0) s₀ τ a ε 0 = ![0, 0, 1] ∧ ∃ (ξ : ↥(EulerTransverseFrameCoordinates.referencePlane Da.m₀)) (lam : ℝ),
ξ ≠ 0 ∧ 0 ≤ lam ∧ lam ≤ 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) / ε ∧ ‖ξ‖ ≤ 8 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * D.inverseBound / h ∧ EulerPacketMovingFrame.scaledVelocity m v
(fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT Ba ξ s 0) τ a ε 0 0 = -lam ∧ EulerPacketMovingFrame.scaledVelocity m v
(fun (s : ℝ) => EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT Ba ξ s 0) τ a ε 0 1 = 1