The literal physical-label bounds feed the source coefficient factory. The constructed child inherits this interface from its proved three-field estimate; frame and coefficient identifications are not extra hypotheses.

structure EulerParentPacketFrames.LabelData (G : Parent) : Type

Label data, collecting K, K_one, displacement, velocity, acceleration, displacement_match and their compatibility conditions.

• K : ℝ

  K of LabelData, of type ℝ.

• K_one : 1 ≤ self.K
• displacement : ↑(Set.Icc 0 G.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Displacement of LabelData, of type Icc (0 : ℝ) G.T → SmoothL2Field Space.

• velocity : ↑(Set.Icc 0 G.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Velocity field of LabelData, of type Icc (0 : ℝ) G.T → SmoothL2Field Space.

• acceleration : ↑(Set.Icc 0 G.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space

  Acceleration of LabelData, of type Icc (0 : ℝ) G.T → SmoothL2Field Space.

• displacement_match (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (self.displacement t).field x = (G.displacement.field t) x
• velocity_match (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (self.velocity t).field x = (G.velocity.field t) x
• acceleration_match (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (self.acceleration t).field x = (G.acceleration.field t) x
• displacement_bound (t : ↑(Set.Icc 0 G.T)) : EulerPacketParentLabelBounds.HasLabelBound self.K (self.displacement t)
• velocity_bound (t : ↑(Set.Icc 0 G.T)) : EulerPacketParentLabelBounds.HasLabelBound self.K (self.velocity t)
• acceleration_bound (t : ↑(Set.Icc 0 G.T)) : EulerPacketParentLabelBounds.HasLabelBound self.K (self.acceleration t)

theorem EulerParentPacketFrames.LabelData.frame_match {G : Parent} (L : LabelData G) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.frame.field t) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (L.displacement t).field (G.ell • x)

theorem EulerParentPacketFrames.LabelData.first_match {G : Parent} (L : LabelData G) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.first.field t) x = fderiv ℝ (L.velocity t).field (G.ell • x)

theorem EulerParentPacketFrames.LabelData.second_match {G : Parent} (L : LabelData G) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : (G.second.field t) x = fderiv ℝ (L.acceleration t).field (G.ell • x)

noncomputable def EulerParentPacketFrames.LabelData.normalBudget {G : Parent} (L : LabelData G) {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) (q : ℕ) : EulerTransversePacketJoin.NormalBudget (G.transverseData m hm R S hS) q (EulerPacketParentNormalBudget.radius (EulerPacketParentLabelBounds.coefficientRadius L.K) (EulerPacketParentLabelBounds.frameAmplitude L.K) (EulerPacketParentLabelBounds.gradientAmplitude L.K))

Normal budget, constructed using EulerPacketParentLabelBudgets.normalBudget.

Equations

• L.normalBudget m hm R S hS q = EulerPacketParentLabelBudgets.normalBudget (G.transverseData m hm R S hS) q L.displacement L.velocity G.ell L.K ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def EulerParentPacketFrames.LabelData.meanBudget {G : Parent} (L : LabelData G) (H : LowBounds G) (q : ℕ) (Ti : ℝ) (hT : G.T ≤ 1) (hTi : G.T⁻¹ ≤ Ti) : EulerMeanPacketProvider.Budget (G.meanData H) q (EulerPacketParentMeanBudget.radius q G.T Ti (EulerPacketParentLabelBounds.coefficientRadius L.K) (EulerPacketParentLabelBounds.frameAmplitude L.K) (EulerPacketParentLabelBounds.gradientAmplitude L.K) (EulerPacketParentLabelBounds.gradientAmplitude L.K) H.L)

Mean budget, constructed using EulerPacketParentLabelBudgets.meanBudget.

Equations

• L.meanBudget H q Ti hT hTi = EulerPacketParentLabelBudgets.meanBudget (G.meanData H) q L.displacement L.velocity L.acceleration Ti L.K hT hTi ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

theorem EulerParentPacketFrames.LabelData.block_nonneg (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (n : ℕ) : 0 ≤ EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction 6 A.toLp ⋯ n

noncomputable def EulerParentPacketFrames.LabelData.child {G : Parent} (L : LabelData G) {P : ℝ} [Fact (0 < P)] (B : EulerPhysicalGraphFlowBounds.Data P G.T) (k : ℝ) (m : EulerSmoothLimit.Space) (hgraph : ∀ (t : ↑(Set.Icc 0 G.T)) (z : EulerLiftedGradientSpace.LiftTangent), (EulerGraphInvariantFlow.graphConstraint k m) ((B.A.field t) z) = 0) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (E : ↑(Set.Icc 0 G.T) → EulerChildParticleFieldBounds.Data) (hD : ∀ (t : ↑(Set.Icc 0 G.T)), (E t).parentDisplacement = L.displacement t) (hV : ∀ (t : ↑(Set.Icc 0 G.T)), (E t).parentVelocity = L.velocity t) (hW : ∀ (t : ↑(Set.Icc 0 G.T)), (E t).parentAcceleration = L.acceleration t) (hd : ∀ (t : ↑(Set.Icc 0 G.T)), (E t).displacement = B.displacementField k m G.ell ⋯ t) (hv : ∀ (t : ↑(Set.Icc 0 G.T)), (E t).velocity = B.velocityField k m G.ell ⋯ t) (hw : ∀ (t : ↑(Set.Icc 0 G.T)), (E t).acceleration = B.accelerationFieldL2 k m G.ell ⋯ t) (K : ℝ) (hK : 1 ≤ K) (hb : ∀ (t : ↑(Set.Icc 0 G.T)) (n : ℕ), EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction 6 (E t).childDisplacement.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction 6 (E t).childVelocity.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction 6 (E t).childAcceleration.toLp ⋯ n ≤ K ^ (n + 1) * ↑n.factorial ^ 2) : LabelData (G.child B k m hgraph nextEll hnext hnext1)

Child as an element of LabelData (G.child B k m hgraph nextEll hnext hnext1).

Equations

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