The concrete compact base Euler solution supplies a uniform polynomial source envelope for its first packet, independent of beta and the support scale.

The genuine short-time forward factory obeys the same source polynomial, using its proved constant profile and physical propagator cost 2.

noncomputable def EulerParentPacketFrames.LabelData.shortForwardCanonicalRadius {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (CM : ℝ) (hCM : 0 ≤ CM) (hM : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖(A.strain.field t) x‖ ≤ CM) (hshort : CM * A.T ≤ 1 / 2) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (ξ : U) : ℝ

Short forward canonical radius, given by EulerPacketForwardRadius.canonicalRadius (J).linear (J).mean (J).normal BC δ ξ.

Equations

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

theorem EulerParentPacketFrames.LabelData.shortForward_radius_primitives {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (CM : ℝ) (hCM : 0 ≤ CM) (hM : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖(A.strain.field t) x‖ ≤ CM) (hshort : CM * A.T ≤ 1 / 2) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (ξ : U) (X : ℝ) (hKX : L.K ≤ X) (hTiX : Ti ≤ X) (hCpX : 2 ≤ X) (hLX : H.L ≤ X) (hδX : δ⁻¹ ≤ X) (hξX : ‖ξ‖ ≤ X) : EulerPacketForwardRadius.RadiusPrimitives (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).linear (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).mean (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).normal (EulerPacketCylinderField.forwardCoefficientBudget EulerPacketTerminalDatum.period (A.meanData H) (A.transverseData m hm R S hS) ⋯ (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).normal) δ ξ (EulerParentInitializedRadius.sourceEnvelope X)

theorem EulerParentPacketFrames.LabelData.shortForward_radius_primitive_polynomial {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {A : Parent} (L : LabelData A) (H : LowBounds A) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (CM : ℝ) (hCM : 0 ≤ CM) (hM : ∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖(A.strain.field t) x‖ ≤ CM) (hshort : CM * A.T ≤ 1 / 2) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (Ti : ℝ) (hT1 : A.T ≤ 1) (hTi : A.T⁻¹ ≤ Ti) (δ : ℝ) (hδ : 0 < δ) (ξ : U) : have X := EulerParentInitializedRadius.parameterSize L.K 0 Ti 2 H.L δ ‖ξ‖; EulerPacketForwardRadius.RadiusPrimitives (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).linear (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).mean (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).normal (EulerPacketCylinderField.forwardCoefficientBudget EulerPacketTerminalDatum.period (A.meanData H) (A.transverseData m hm R S hS) ⋯ (L.forwardInputs H m hm R S hS CM hCM hM Ω hΩ hΩo hsub hΩball hshort Ti hT1 hTi).normal) δ ξ (EulerParentInitializedRadius.sourceEnvelope X) ∧ EulerParentInitializedRadius.sourceEnvelope X ≤ EulerParentInitializedRadius.sourceConstant * X ^ EulerParentInitializedRadius.sourcePower

noncomputable def EulerBaseDatum.firstParameterSize (T δ hchild : ℝ) : ℝ

First parameter size, given by 4+solutionLabelConstant+T⁻¹+δ⁻¹+hchild.

Equations

• EulerBaseDatum.firstParameterSize T δ hchild = 4 + EulerBaseDatum.solutionLabelConstant + T⁻¹ + δ⁻¹ + hchild

theorem EulerBaseDatum.firstParameterSize_bounds (T δ hchild : ℝ) (hT : 0 < T) (hδ : 0 < δ) (hh : 0 ≤ hchild) : 1 ≤ firstParameterSize T δ hchild ∧ solutionLabelConstant ≤ firstParameterSize T δ hchild ∧ T⁻¹ ≤ firstParameterSize T δ hchild ∧ 2 ≤ firstParameterSize T δ hchild ∧ δ⁻¹ ≤ firstParameterSize T δ hchild ∧ hchild ≤ firstParameterSize T δ hchild

theorem EulerBaseDatum.firstPacket_uniform_primitives (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hchild : ℝ) (hh : 0 ≤ hchild) : have X := firstParameterSize T δ hchild; EulerPacketForwardRadius.RadiusPrimitives (firstPacketInputs β hβ ell hell hell1 T hT hTB).linear (firstPacketInputs β hβ ell hell hell1 T hT hTB).mean (firstPacketInputs β hβ ell hell hell1 T hT hTB).normal (EulerPacketCylinderField.forwardCoefficientBudget EulerPacketTerminalDatum.period ((packetBaseParent β hβ ell hell hell1 T hT hTB).meanData (packetBaseLowBounds β hβ ell hell hell1 T hT hTB)) ((packetBaseParent β hβ ell hell hell1 T hT hTB).transverseData firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact) ⋯ (firstPacketInputs β hβ ell hell hell1 T hT hTB).normal) δ firstCoordinate (EulerPacketUniformSource.profileEnvelope X) ∧ (∀ (t : ↑(Set.Icc 0 ((packetBaseParent β hβ ell hell hell1 T hT hTB).transverseData firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact).T)), δ * hchild * (firstPacketInputs β hβ ell hell hell1 T hT hTB).linear.g t ≤ EulerPacketUniformSource.profileEnvelope X) ∧ EulerPacketInitializedOutputCost.uniformConstant * EulerPacketUniformSource.profileEnvelope X ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketUniformSource.frequencyConstant * X ^ EulerPacketUniformSource.frequencyPower