Literal forward and joined source guards for the next packet of an actual finite stage. The radius is one, the spike and target shear are the prescribed source scales, and the physical target is nextTime.
The actual next packet geometry is constructed from the current finite stage. Source normals, history bounds and the neighboring-label guards are derived from its state and the one fixed scale choice.
The source direction at a stage is constructed from the actual parent deformation and older frame. Both branch-specific normal-choice identities are conclusions, and the reference plane is literal.
Changing the source normal and reference plane leaves the older physical frame and its scalar parameters unchanged. The source strain and time interval are the actual fields of the same parent.
def
EulerPacketSourceGeometry.ParentFrame.reframe
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
ParentFrame (A.transverseData m' hm' R' S hS) τ
Reframe, bundling B, B₁, m, v and the required compatibility proofs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_B
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_B₁
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_m
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_v
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_c
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_G
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_error
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_a
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_sigma
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_shear
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_epsilon
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_horizon
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_rayScale
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
(hτ : 0 < τ)
(hτT : τ < A.T)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.reframe_terminalBound
{A : EulerParentPacketFrames.Parent}
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
(CM CH : ℝ)
:
theorem
EulerParentPacketFrames.Parent.transverse_deformation_reframe
(A : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
{V : Type u_2}
[NormedAddCommGroup V]
[InnerProductSpace ℝ V]
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
(R' : V ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m'))
(t : ↑(Set.Icc 0 A.T))
(x : EulerSmoothLimit.Space)
:
(A.transverseData m' hm' R' S hS).deformationEquiv t x = (A.transverseData m hm R S hS).deformationEquiv t x
theorem
EulerParentPacketFrames.Parent.transverse_reframe
(A : Parent)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(m' : EulerSmoothLimit.Space)
(hm' : ‖m'‖ = 1)
:
(A.transverseData m hm R S hS).reframe m' hm' = A.transverseData m' hm' (LinearIsometryEquiv.refl ℝ ↥(EulerTransverseFrameCoordinates.referencePlane m')) S hS
noncomputable def
EulerPacketSourceGeometry.ParentFrame.crossDirection
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
:
Cross direction, given by cross (unit (P.m τ)) (unit (P.v τ)).
Equations
Instances For
theorem
EulerPacketSourceGeometry.ParentFrame.crossDirection_unit
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτT : τ ≤ A.T)
:
theorem
EulerPacketSourceGeometry.ParentFrame.crossDirection_ne_zero
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτT : τ ≤ A.T)
:
noncomputable def
EulerPacketSourceGeometry.ParentFrame.activationNormal
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
Activation normal, given by activationDirection ((A.transverseData m hm R S hS).deformationEquiv ⟨τ,hτ.le,hτT.le⟩ 0) P.crossDirection.
Equations
- P.activationNormal hτ hτT = EulerPacketMovingFrame.activationDirection ((A.transverseData m hm R S hS).deformationEquiv ⟨τ, ⋯⟩ 0) P.crossDirection
Instances For
theorem
EulerPacketSourceGeometry.ParentFrame.activationNormal_unit
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
noncomputable def
EulerPacketSourceGeometry.ParentFrame.activationData
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
Activation data, constructed using A.transverseData.
Equations
- P.activationData hτ hτT = A.transverseData (P.activationNormal hτ hτT) ⋯ (LinearIsometryEquiv.refl ℝ ↥(EulerTransverseFrameCoordinates.referencePlane (P.activationNormal hτ hτT))) S hS
Instances For
noncomputable def
EulerPacketSourceGeometry.ParentFrame.activationFrame
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
ParentFrame (P.activationData hτ hτT) τ
Activation frame, constructed using P.reframe.
Equations
- P.activationFrame hτ hτT = P.reframe (P.activationNormal hτ hτT) ⋯ (LinearIsometryEquiv.refl ℝ ↥(EulerTransverseFrameCoordinates.referencePlane (P.activationNormal hτ hτT)))
Instances For
theorem
EulerPacketSourceGeometry.ParentFrame.activation_normal_choice
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
(P.activationData hτ hτT).m₀ = EulerPacketMovingFrame.activationDirection ((P.activationData hτ hτT).deformationEquiv ⟨τ, ⋯⟩ 0)
(EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit ((P.activationFrame hτ hτT).m τ))
(EulerPacketNormalizedPrimary.unit ((P.activationFrame hτ hτT).v τ)))
theorem
EulerPacketSourceGeometry.ParentFrame.activation_parameters
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
(P.activationFrame hτ hτT).a = P.a ∧ (P.activationFrame hτ hτT).sigma = P.sigma ∧ (P.activationFrame hτ hτT).shear = P.shear ∧ (P.activationFrame hτ hτT).epsilon = P.epsilon ∧ (P.activationFrame hτ hτT).horizon = P.horizon ∧ (P.activationFrame hτ hτT).G = P.G ∧ (P.activationFrame hτ hτT).error = P.error
theorem
EulerPacketSourceGeometry.ParentFrame.activation_ray
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
The new covector really transports to the old frame's cross direction, with the same strictly positive ray scale used by Guards.
theorem
EulerPacketSourceGeometry.ParentFrame.activation_scaled_ray
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
:
noncomputable def
EulerPacketSourceGeometry.ParentFrame.activationHistory
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
(H : EulerParentPacketFrames.LowBounds A)
:
EulerTransversePacketProvider.HistoryData ((P.activationData hτ hτT).initial τ hτ ⋯)
Activation history, constructed using A.historyOn.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketSourceGeometry.ParentFrame.activation_history_eq
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
{τ : ℝ}
(P : ParentFrame (A.transverseData m hm R S hS) τ)
(hτ : 0 < τ)
(hτT : τ < A.T)
(H : EulerParentPacketFrames.LowBounds A)
:
P.activationHistory hτ hτT H = (A.historyOn H m hm R S hS τ hτ hτT).reframe (P.activationNormal hτ hτT) ⋯
noncomputable def
EulerPacketSourceGeometry.ParentFrame.forwardData
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
(P : ParentFrame (A.transverseData m hm R S hS) 0)
:
Forward data, constructed using A.transverseData.
Equations
Instances For
noncomputable def
EulerPacketSourceGeometry.ParentFrame.forwardFrame
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
(P : ParentFrame (A.transverseData m hm R S hS) 0)
:
Forward frame, given by P.reframe P.crossDirection (P.crossDirection_unit A.T_pos.le) (LinearIsometryEquiv.refl ℝ (referencePlane P.crossDirection)).
Equations
Instances For
theorem
EulerPacketSourceGeometry.ParentFrame.forward_normal_choice
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
(P : ParentFrame (A.transverseData m hm R S hS) 0)
:
theorem
EulerPacketSourceGeometry.ParentFrame.forward_initial_frame
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
(P : ParentFrame (A.transverseData m hm R S hS) 0)
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketSourceGeometry.ParentFrame.forward_initial_normal
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
(P : ParentFrame (A.transverseData m hm R S hS) 0)
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketSourceGeometry.ParentFrame.forward_parameters
{A : EulerParentPacketFrames.Parent}
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{m : EulerSmoothLimit.Space}
{hm : ‖m‖ = 1}
{R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)}
{S : Set EulerSmoothLimit.Space}
{hS : IsCompact S}
(P : ParentFrame (A.transverseData m hm R S hS) 0)
:
P.forwardFrame.a = P.a ∧ P.forwardFrame.sigma = P.sigma ∧ P.forwardFrame.shear = P.shear ∧ P.forwardFrame.epsilon = P.epsilon ∧ P.forwardFrame.horizon = P.horizon ∧ P.forwardFrame.G = P.G ∧ P.forwardFrame.error = P.error
def
EulerPacketSourceGeometry.ParentFrame.changeActivation
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
ParentFrame D t
Change activation, given by h ▸ P.
Equations
- P.changeActivation h = h ▸ P
Instances For
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_a
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_sigma
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_shear
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_G
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_error
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_horizon
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_B
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_m
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
@[simp]
theorem
EulerPacketSourceGeometry.ParentFrame.changeActivation_v
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{s t : ℝ}
(P : ParentFrame D s)
(h : s = t)
:
theorem
EulerPacketInduction.Stage.history_layer
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
noncomputable def
EulerPacketInduction.Stage.joinedNormal
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
Joined normal, given by P.restrictedFrame.activationNormal (P.time_pos hn) P.time_lt_nextHorizon.
Equations
- P.joinedNormal hn = P.restrictedFrame.activationNormal ⋯ ⋯
Instances For
theorem
EulerPacketInduction.Stage.joinedNormal_unit
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
noncomputable def
EulerPacketInduction.Stage.joinedData
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
Joined data, given by P.restrictedFrame.activationData (P.time_pos hn) P.time_lt_nextHorizon.
Equations
- P.joinedData hn = P.restrictedFrame.activationData ⋯ ⋯
Instances For
noncomputable def
EulerPacketInduction.Stage.joinedFrame
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
Joined frame, given by P.restrictedFrame.activationFrame (P.time_pos hn) P.time_lt_nextHorizon.
Equations
- P.joinedFrame hn = P.restrictedFrame.activationFrame ⋯ ⋯
Instances For
noncomputable def
EulerPacketInduction.Stage.joinedHistory
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
EulerTransversePacketProvider.HistoryData ((P.joinedData hn).initial P.time ⋯ ⋯)
Joined history, given by P.restrictedFrame.activationHistory (P.time_pos hn) P.time_lt_nextHorizon P.restrictedLow.
Equations
- P.joinedHistory hn = P.restrictedFrame.activationHistory ⋯ ⋯ P.restrictedLow
Instances For
@[simp]
theorem
EulerPacketInduction.Stage.joinedFrame_a
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedFrame_sigma
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedFrame_shear
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedFrame_G
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedFrame_error
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedFrame_horizon
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
theorem
EulerPacketInduction.Stage.joined_history_strain
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
theorem
EulerPacketInduction.Stage.joined_history_hessian
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
:
noncomputable def
EulerPacketInduction.Stage.zeroFrame
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
Zero frame, given by P.restrictedFrame.changeActivation (P.time_zero rfl).
Equations
Instances For
noncomputable def
EulerPacketInduction.Stage.forwardNormal
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
Forward normal, given by P.zeroFrame.crossDirection.
Equations
Instances For
theorem
EulerPacketInduction.Stage.forwardNormal_unit
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
noncomputable def
EulerPacketInduction.Stage.forwardData
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
Forward data, given by P.zeroFrame.forwardData.
Equations
Instances For
noncomputable def
EulerPacketInduction.Stage.forwardFrame
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
Forward frame, given by P.zeroFrame.forwardFrame.
Equations
Instances For
@[simp]
theorem
EulerPacketInduction.Stage.forwardFrame_a
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardFrame_sigma
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardFrame_shear
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardFrame_G
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardFrame_error
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardFrame_horizon
{c B : ℝ}
{S : EulerPacketInductionScales.Scales c B}
(P : Stage S 0)
:
Reciprocal history times fit the literal previous-frequency budget. Only the first geometric step needs coupling and tilt bounds. All later step lengths are nonnegative independently of any future frame invariant.
theorem
EulerParentHistoryFrequency.activation_lower_of_initial
(J : ℕ)
(hJ : 1 ≤ J)
(X : ℝ)
(hX : 0 < X)
(a β : ℕ → ℝ)
(ha : 1 / 2 ≤ a 0)
(ha₂ : a 0 ≤ 2)
(hβ : 1 / 2 ≤ β 0 * X ^ 2)
(hβ₂ : β 0 * X ^ 2 ≤ 2)
{n : ℕ}
(hn : 1 ≤ n)
:
EulerPacketBaseGuardScales.baseHorizon J X / 12 ≤ EulerPacketNestedHorizons.activationTime J X a β n
theorem
EulerParentHistoryFrequency.reciprocal_activation_le_base
(J : ℕ)
(hJ : 1 ≤ J)
(X : ℝ)
(hX : 0 < X)
(a β : ℕ → ℝ)
(ha : 1 / 2 ≤ a 0)
(ha₂ : a 0 ≤ 2)
(hβ : 1 / 2 ≤ β 0 * X ^ 2)
(hβ₂ : β 0 * X ^ 2 ≤ 2)
{n : ℕ}
(hn : 1 ≤ n)
:
(EulerPacketNestedHorizons.activationTime J X a β n)⁻¹ ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X
theorem
EulerParentHistoryFrequency.actual_reciprocal_activation
(J D : ℕ)
(hJ : 3 ≤ J)
(hD : 2000 ≤ D)
(C c X δ : ℝ)
(hX : 2 ≤ X)
(hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ)
(a β : ℕ → ℝ)
(ha : 1 / 2 ≤ a 0)
(ha₂ : a 0 ≤ 2)
(hβ : 1 / 2 ≤ β 0 * X ^ 2)
(hβ₂ : β 0 * X ^ 2 ≤ 2)
{n : ℕ}
(hn : 1 ≤ n)
:
(EulerPacketNestedHorizons.activationTime J X a β n)⁻¹ ≤ 12 / EulerPacketBaseGuardScales.baseHorizon J X ∧ 12 / EulerPacketBaseGuardScales.baseHorizon J X ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ 80
The literal numerical scale guards also initialize the zero-history amplification stage. Its new ray and velocity start exactly in the old frame, so only the actual strain's spatial variation enters the error.
theorem
EulerParentPacketFrames.LabelData.forwardError_bound
{A : Parent}
(L : LabelData A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R support hSupport) 0)
(ρ E N : ℝ)
(hρ : 0 ≤ ρ)
(hE : P.error ≤ E)
(hN : L.strainDifferenceCost * A.ell * ρ ≤ N)
:
noncomputable def
EulerParentPacketFrames.LabelData.forwardGeometryGuardsOfStage
{A : Parent}
(L : LabelData A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(P : EulerPacketSourceGeometry.ParentFrame (A.transverseData m hm R support hSupport) 0)
(J D : ℕ)
(C c X : ℝ)
(a β : ℕ → ℝ)
(n : ℕ)
(CF : ℝ)
(hCF : 1 ≤ CF)
(stage :
EulerPacketSourceScaleGuards.StageGuards J D C c X (EulerPacketMovingFrame.neighborStabilityConstant * CF ^ 2) a β n)
(ha : 1 / 2 ≤ a n)
(ha_match : P.a = a n)
(hshear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n)
(hsigma : P.sigma = √(β n))
(htime : P.horizon = EulerPacketSourceScaleGuards.horizon J X (a n) (β n) n)
(hG : P.G ≤ CF * (1 + EulerPacketSourceScaleSequence.olderShear J X n))
(herr : P.error ≤ EulerPacketSourceScaleActual.priorError J D X n)
(ρ δ hchild : ℝ)
(hρ : 0 ≤ ρ)
(hδ : 0 ≤ δ)
(hhchild : 0 ≤ hchild)
(hneighbor : L.strainDifferenceCost * A.ell * ρ ≤ EulerPacketSourceScaleActual.neighborError J D X c n)
(hnormal :
m = EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (P.m 0))
(EulerPacketNormalizedPrimary.unit (P.v 0)))
:
Forward geometry guards of stage as an element of ForwardGuards P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The computed neighboring-label cost fits the source's monomial majorant under fixed degree and constant guards. Thus the small support scale discharges the literal neighbor comparison in the geometry step.
theorem
EulerParentPacketFrames.LabelData.neighborScaleCost_monomial
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(Ti CM CH : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hCM : 0 ≤ CM)
(hCH : 0 ≤ CH)
(ha : 1 / 2 ≤ P.a)
(hH : 1 ≤ P.shear)
(k : ℝ)
(q c : ℕ)
(hk : 1 ≤ k)
(hKk : L.K ≤ k ^ q)
(hTik : Ti ≤ k ^ q)
(hcost :
EulerParentNeighborCost.boundConstant * (2 * (1 + CM + CH)) ^ EulerParentNeighborCost.degree * 4 ^ EulerParentNeighborCost.degree ≤ k)
(hc : q * EulerParentNeighborCost.degree + 1 ≤ c)
(hn : EulerParentNeighborCost.degree ≤ c)
:
theorem
EulerParentPacketFrames.LabelData.neighbor_error_of_source_scales
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(Ti CM CH : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hCM : 0 ≤ CM)
(hCH : 0 ≤ CH)
(ha : 1 / 2 ≤ P.a)
(hH : 1 ≤ P.shear)
(J D : ℕ)
(X ρ : ℝ)
(j q c : ℕ)
(hρ : 0 ≤ ρ)
(hρ1 : ρ ≤ 1)
(hshear : P.shear = EulerPacketSourceScaleSequence.previousShear J X j)
(hk : 1 ≤ EulerPacketSourceScaleSequence.previousFrequency J D X j)
(hKk : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X j ^ q)
(hTik : Ti ≤ EulerPacketSourceScaleSequence.previousFrequency J D X j ^ q)
(hcost :
EulerParentNeighborCost.boundConstant * (2 * (1 + CM + CH)) ^ EulerParentNeighborCost.degree * 4 ^ EulerParentNeighborCost.degree ≤ EulerPacketSourceScaleSequence.previousFrequency J D X j)
(hc : q * EulerParentNeighborCost.degree + 1 ≤ c)
(hn : EulerParentNeighborCost.degree ≤ c)
(hscale : G.ell ≤ EulerPacketSourceScaleSequence.supportScale J X j)
:
L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH * G.ell * ρ ≤ EulerPacketSourceScaleActual.neighborError J D X (↑c) j
Fixed coefficient thresholds for the literal neighboring-label guard. The history reciprocal is derived from the initial geometric step, and the only parent size input is the already constructed parent's label bound.
Forward threshold, given by boundConstant*4^degree.
Equations
Instances For
Joined threshold, given by (boundConstant*(2*(1+CM+CH))^degree)*4^degree.
Equations
Instances For
Required exponent, given by 80*degree+1.
Instances For
theorem
EulerParentPacketFrames.LabelData.strainDifferenceCost_monomial
{G : Parent}
(L : LabelData G)
(k : ℝ)
(c : ℕ)
(hk : 1 ≤ k)
(hKk : L.K ≤ k ^ 80)
(hcost : EulerParentNeighborThreshold.forwardThreshold ≤ k)
(hc : EulerParentNeighborThreshold.requiredExponent ≤ c)
:
theorem
EulerParentPacketFrames.LabelData.forward_neighbor_error_of_source_scales
{G : Parent}
(L : LabelData G)
(J D : ℕ)
(hJ : 3 ≤ J)
(X ρ : ℝ)
(hX : 1 ≤ X)
(hbase : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4))
(n c : ℕ)
(hρ : 0 ≤ ρ)
(hρ1 : ρ ≤ 1)
(hKk : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ 80)
(hcost : EulerParentNeighborThreshold.forwardThreshold ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n)
(hc : EulerParentNeighborThreshold.requiredExponent ≤ c)
(hscale : G.ell ≤ EulerPacketSourceScaleSequence.supportScale J X n)
:
theorem
EulerParentPacketFrames.LabelData.joined_neighbor_error_of_literal_scales
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(J D : ℕ)
(hJ : 3 ≤ J)
(hD : 2000 ≤ D)
(X ρ CM CH : ℝ)
(hX : 2 ≤ X)
(hbase : X ^ D ≤ Real.exp (X / ↑(J - 1) ^ 4))
(a β : ℕ → ℝ)
(ha₀ : 1 / 2 ≤ a 0)
(ha₀₂ : a 0 ≤ 2)
(hβ₀ : 1 / 2 ≤ β 0 * X ^ 2)
(hβ₀₂ : β 0 * X ^ 2 ≤ 2)
(n c : ℕ)
(hn : 1 ≤ n)
(hτliteral : τ = EulerPacketNestedHorizons.activationTime J X a β n)
(hτ1 : τ ≤ 1)
(hCM : 0 ≤ CM)
(hCH : 0 ≤ CH)
(ha : 1 / 2 ≤ P.a)
(hH : 1 ≤ P.shear)
(hρ : 0 ≤ ρ)
(hρ1 : ρ ≤ 1)
(hshear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n)
(hKk : L.K ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n ^ 80)
(hcost : EulerParentNeighborThreshold.joinedThreshold CM CH ≤ EulerPacketSourceScaleSequence.previousFrequency J D X n)
(hc : EulerParentNeighborThreshold.requiredExponent ≤ c)
(hscale : G.ell ≤ EulerPacketSourceScaleSequence.supportScale J X n)
:
L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH * G.ell * ρ ≤ EulerPacketSourceScaleActual.neighborError J D X (↑c) n
theorem
EulerPacketInduction.Stage.joined_neighbor
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
P.restrictedState.labels.neighborScaleCost (P.joinedNormal hn) ⋯
(LinearIsometryEquiv.refl ℝ ↥(EulerTransverseFrameCoordinates.referencePlane (P.joinedNormal hn)))
EulerPacketSupport.support EulerPacketSupport.compact P.restrictedLow P.time ⋯ ⋯ (P.joinedFrame hn)
EulerPacketLowConstants.gradientConstant EulerPacketLowConstants.hessianConstant * P.restrictedParent.ell * 1 ≤ EulerPacketSourceScaleActual.neighborError S.J S.D S.X (↑q) n
noncomputable def
EulerPacketInduction.Stage.joinedGuards
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
EulerPacketSourceGeometry.Guards ⋯ ⋯ (P.joinedFrame hn) (P.joinedHistory hn)
Joined guards, constructed using P.restrictedState.labels.geometryGuardsOfStage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
EulerPacketInduction.Stage.joinedGuards_radius
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedGuards_y
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedGuards_delta
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedGuards_shear
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedGuards_CM
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.joinedGuards_CH
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
theorem
EulerPacketInduction.Stage.joined_source_neighbor
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
(P.joinedFrame hn).neighborCost ⋯ ⋯ (P.joinedHistory hn) (P.joinedGuards hn hq hB).CM (P.joinedGuards hn hq hB).CH * (P.joinedGuards hn hq hB).radius ≤ EulerPacketSourceScaleActual.neighborError S.J S.D S.X (↑q) n
noncomputable def
EulerPacketInduction.Stage.joinedGeometry
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
Joined geometry, given by (P.joinedGuards hn hq hB).lowGeometry (by rw [P.joinedGuards_radius]; norm_num).
Equations
- P.joinedGeometry hn hq hB = (P.joinedGuards hn hq hB).lowGeometry ⋯
Instances For
theorem
EulerPacketInduction.Stage.joinedGeometry_targetTime
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
{n : ℕ}
(P : Stage S n)
(hn : n ≠ 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
theorem
EulerPacketInduction.Stage.forward_neighbor
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
P.restrictedState.labels.strainDifferenceCost * P.restrictedParent.ell * 1 ≤ EulerPacketSourceScaleActual.neighborError S.J S.D S.X (↑q) 0
noncomputable def
EulerPacketInduction.Stage.forwardGuards
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
Forward guards, constructed using P.restrictedState.labels.forwardGeometryGuardsOfStage.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
EulerPacketInduction.Stage.forwardGuards_radius
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardGuards_y
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardGuards_delta
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
@[simp]
theorem
EulerPacketInduction.Stage.forwardGuards_shear
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
theorem
EulerPacketInduction.Stage.forward_source_neighbor
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
‖P.forwardData.M.derivative.field‖ * (P.forwardGuards hq hB).radius ≤ EulerPacketSourceScaleActual.neighborError S.J S.D S.X (↑q) 0
noncomputable def
EulerPacketInduction.Stage.forwardGeometry
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
:
Forward geometry, given by (P.forwardGuards hq hB).lowGeometry (by rw [P.forwardGuards_radius]; norm_num).
Equations
- P.forwardGeometry hq hB = (P.forwardGuards hq hB).lowGeometry ⋯
Instances For
theorem
EulerPacketInduction.Stage.forwardGeometry_targetTime
{q : ℕ}
{B : ℝ}
{S : EulerPacketInductionScales.Scales (↑q) B}
(P : Stage S 0)
(hq : EulerParentNeighborThreshold.requiredExponent ≤ q)
(hB :
EulerParentNeighborThreshold.commonThreshold EulerPacketLowConstants.gradientConstant
EulerPacketLowConstants.hessianConstant ≤ B)
: