Polynomial control of the literal canonical initialized radius built from the parent fields. The boundary coefficient remains an explicit scalar input.

A fixed polynomial in the genuine parent label bound controls the coefficient leaves of the normal, joined and mean packet budgets.

def EulerParentCoefficientPolynomial.radiusCeiling (K : ℝ) : ℝ

Radius ceiling, given by 1024+4*K.

Equations

• EulerParentCoefficientPolynomial.radiusCeiling K = 1024 + 4 * K

noncomputable def EulerParentCoefficientPolynomial.curvatureCeiling (K : ℝ) : ℝ

Curvature ceiling, given by 27*(frameAmplitude K)^2*gradientAmplitude K.

Equations

• EulerParentCoefficientPolynomial.curvatureCeiling K = 27 * EulerPacketParentLabelBounds.frameAmplitude K ^ 2 * EulerPacketParentLabelBounds.gradientAmplitude K

noncomputable def EulerParentCoefficientPolynomial.normalAmplitude (K : ℝ) : ℝ

Normal amplitude, given by EulerPacketParentNormalBudget.amplitude (frameAmplitude K) (gradientAmplitude K).

Equations

• EulerParentCoefficientPolynomial.normalAmplitude K = EulerPacketParentNormalBudget.amplitude (EulerPacketParentLabelBounds.frameAmplitude K) (EulerPacketParentLabelBounds.gradientAmplitude K)

noncomputable def EulerParentCoefficientPolynomial.normalInverse (K : ℝ) : ℝ

Normal inverse, given by EulerPacketParentNormalBudget.inverseRadius (radiusCeiling K) (frameAmplitude K) (gradientAmplitude K).

Equations

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

noncomputable def EulerParentCoefficientPolynomial.normalRadius (K : ℝ) : ℝ

Normal radius, given by EulerPacketParentNormalBudget.radius (radiusCeiling K) (frameAmplitude K) (gradientAmplitude K).

Equations

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

noncomputable def EulerParentCoefficientPolynomial.transverseInverse (K : ℝ) : ℝ

Transverse inverse, given by EulerPacketParentTransverseCosts.inverseRadius (radiusCeiling K) (frameAmplitude K).

Equations

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

noncomputable def EulerParentCoefficientPolynomial.leafEnvelope (K : ℝ) : ℝ

Leaf envelope as an element of ℝ.

Equations

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

noncomputable def EulerParentCoefficientPolynomial.leafPolynomial : Polynomial ℝ

Leaf polynomial as an element of Polynomial ℝ.

Equations

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

theorem EulerParentCoefficientPolynomial.leafPolynomial_eval (K : ℝ) : Polynomial.eval K leafPolynomial = leafEnvelope K

noncomputable def EulerParentCoefficientPolynomial.leafConstant : ℝ

Leaf constant, given by coefficientCost leafPolynomial.

Equations

• EulerParentCoefficientPolynomial.leafConstant = EulerPolynomialCost.coefficientCost EulerParentCoefficientPolynomial.leafPolynomial

noncomputable def EulerParentCoefficientPolynomial.leafPower : ℕ

Leaf power, given by leafPolynomial.natDegree.

Equations

• EulerParentCoefficientPolynomial.leafPower = EulerParentCoefficientPolynomial.leafPolynomial.natDegree

theorem EulerParentCoefficientPolynomial.leafConstant_pos : 0 < leafConstant

theorem EulerParentCoefficientPolynomial.leafEnvelope_power (K : ℝ) (hK : 1 ≤ K) : leafEnvelope K ≤ leafConstant * K ^ leafPower

theorem EulerParentCoefficientPolynomial.radiusCeiling_le (K : ℝ) (hK : 0 ≤ K) : EulerPacketParentLabelBounds.coefficientRadius K ≤ radiusCeiling K

theorem EulerParentCoefficientPolynomial.leaf_bounds (K : ℝ) (hK : 0 ≤ K) : 1 ≤ leafEnvelope K ∧ EulerPacketParentLabelBounds.coefficientRadius K ≤ leafEnvelope K ∧ EulerPacketParentLabelBounds.gradientAmplitude K ≤ leafEnvelope K ∧ EulerPacketParentLabelBounds.frameAmplitude K ≤ leafEnvelope K ∧ curvatureCeiling K ≤ leafEnvelope K ∧ normalAmplitude K ≤ leafEnvelope K ∧ EulerPacketParentNormalBudget.inverseRadius (EulerPacketParentLabelBounds.coefficientRadius K) (EulerPacketParentLabelBounds.frameAmplitude K) (EulerPacketParentLabelBounds.gradientAmplitude K) ≤ leafEnvelope K ∧ EulerPacketParentNormalBudget.radius (EulerPacketParentLabelBounds.coefficientRadius K) (EulerPacketParentLabelBounds.frameAmplitude K) (EulerPacketParentLabelBounds.gradientAmplitude K) ≤ leafEnvelope K ∧ EulerPacketParentMeanCoercivity.gramInverseEnvelope (EulerPacketParentLabelBounds.frameAmplitude K) ≤ leafEnvelope K ∧ EulerPacketParentTransverseCosts.inverseRadius (EulerPacketParentLabelBounds.coefficientRadius K) (EulerPacketParentLabelBounds.frameAmplitude K) ≤ leafEnvelope K ∧ EulerPacketParentMeanCoercivity.inverseEnvelope (EulerPacketParentLabelBounds.frameAmplitude K) (EulerPacketParentLabelBounds.gradientAmplitude K) ≤ leafEnvelope K

theorem EulerParentCoefficientPolynomial.frameLower_inv_le {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (K : ℝ) (hK : 0 ≤ K) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ EulerPacketParentLabelBounds.frameAmplitude K) : D.frameLower⁻¹ ≤ leafEnvelope K

Composing the actual coefficient envelope with the parent label polynomial gives a single fixed polynomial in the parent size K.

noncomputable def EulerParentCorrectionCost.parentEnvelope (P : ℝ) [Fact (0 < P)] (K : ℝ) : ℝ

Parent envelope, given by 1+leafEnvelope K+primitiveEnvelope P (leafEnvelope K).

Equations

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

noncomputable def EulerParentCorrectionCost.parentPolynomial (P : ℝ) [Fact (0 < P)] : Polynomial ℝ

Parent polynomial, given by 1+leafPolynomial+(primitivePolynomial P).comp leafPolynomial.

Equations

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

noncomputable def EulerParentCorrectionCost.parentConstant (P : ℝ) [Fact (0 < P)] : ℝ

Parent constant, given by coefficientCost (parentPolynomial P).

Equations

• EulerParentCorrectionCost.parentConstant P = EulerPolynomialCost.coefficientCost (EulerParentCorrectionCost.parentPolynomial P)

noncomputable def EulerParentCorrectionCost.parentPower (P : ℝ) [Fact (0 < P)] : ℕ

Parent power, given by (parentPolynomial P).natDegree.

Equations

• EulerParentCorrectionCost.parentPower P = (EulerParentCorrectionCost.parentPolynomial P).natDegree

theorem EulerParentCorrectionCost.parentConstant_pos (P : ℝ) [Fact (0 < P)] : 0 < parentConstant P

theorem EulerParentCorrectionCost.parentPolynomial_eval (P : ℝ) [Fact (0 < P)] (K : ℝ) : Polynomial.eval K (parentPolynomial P) = parentEnvelope P K

theorem EulerParentCorrectionCost.parentEnvelope_power (P : ℝ) [Fact (0 < P)] (K : ℝ) (hK : 1 ≤ K) : parentEnvelope P K ≤ parentConstant P * K ^ parentPower P

theorem EulerParentCorrectionCost.parentEnvelope_bounds (P : ℝ) [Fact (0 < P)] (K : ℝ) (hK : 0 ≤ K) : 1 ≤ parentEnvelope P K ∧ EulerParentCoefficientPolynomial.leafEnvelope K ≤ parentEnvelope P K ∧ EulerPacketCorrectionPrimitive.primitiveEnvelope P (EulerParentCoefficientPolynomial.leafEnvelope K) ≤ parentEnvelope P K

theorem EulerPacketCylinderField.CoefficientBudget.parent_primitive_bound {P T : ℝ} [Fact (0 < P)] {O : EulerPacketProfileRecursion.Operators} {C : CoefficientData P T O} (B : CoefficientBudget C) (K : ℝ) (hK : 0 ≤ K) (hR : B.Rc ≤ EulerParentCoefficientPolynomial.leafEnvelope K) (hC : B.amplitude ≤ EulerParentCoefficientPolynomial.leafEnvelope K) : B.multiplierCost ≤ EulerParentCorrectionCost.parentEnvelope P K ∧ B.termCost ≤ EulerParentCorrectionCost.parentEnvelope P K

noncomputable def EulerParentInitializedRadius.inputEnvelope (X : ℝ) : ℝ

Input envelope, given by let a := parentConstant period*X^parentPower period 1+X+a+3*a^3*X.

Equations

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

noncomputable def EulerParentInitializedRadius.inputPolynomial : Polynomial ℝ

Input polynomial, given by let X : Polynomial ℝ := Polynomial.X let a := Polynomial.C (parentConstant period)*X^parentPower period 1+X+a+3*a^3*X.

Equations

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

theorem EulerParentInitializedRadius.inputPolynomial_eval (X : ℝ) : Polynomial.eval X inputPolynomial = inputEnvelope X

theorem EulerParentInitializedRadius.inputEnvelope_bounds (K X : ℝ) (hK : 1 ≤ K) (hKX : K ≤ X) : 1 ≤ inputEnvelope X ∧ X ≤ inputEnvelope X ∧ EulerParentCoefficientPolynomial.leafEnvelope K ≤ inputEnvelope X ∧ EulerParentCorrectionCost.parentEnvelope EulerPacketTerminalDatum.period K ≤ inputEnvelope X ∧ ∀ (Cp : ℝ), 0 ≤ Cp → Cp ≤ X → EulerPacketParentPhysicalBudgets.physicalCost K Cp ≤ inputEnvelope X

noncomputable def EulerParentInitializedRadius.sourceEnvelope (X : ℝ) : ℝ

Source envelope, given by sourceRadiusEnvelope (inputEnvelope X).

Equations

• EulerParentInitializedRadius.sourceEnvelope X = EulerPacketSourceRadius.sourceRadiusEnvelope (EulerParentInitializedRadius.inputEnvelope X)

noncomputable def EulerParentInitializedRadius.sourcePolynomial : Polynomial ℝ

Source polynomial, given by sourceRadiusPolynomial.comp inputPolynomial.

Equations

• EulerParentInitializedRadius.sourcePolynomial = EulerPacketSourceRadius.sourceRadiusPolynomial.comp EulerParentInitializedRadius.inputPolynomial

theorem EulerParentInitializedRadius.sourcePolynomial_eval (X : ℝ) : Polynomial.eval X sourcePolynomial = sourceEnvelope X

noncomputable def EulerParentInitializedRadius.sourceConstant : ℝ

Source constant, given by coefficientCost sourcePolynomial.

Equations

• EulerParentInitializedRadius.sourceConstant = EulerPolynomialCost.coefficientCost EulerParentInitializedRadius.sourcePolynomial

noncomputable def EulerParentInitializedRadius.sourcePower : ℕ

Source power, given by sourcePolynomial.natDegree.

Equations

• EulerParentInitializedRadius.sourcePower = EulerParentInitializedRadius.sourcePolynomial.natDegree

theorem EulerParentInitializedRadius.sourceConstant_pos : 0 < sourceConstant

theorem EulerParentInitializedRadius.sourceEnvelope_power (X : ℝ) (hX : 1 ≤ X) : sourceEnvelope X ≤ sourceConstant * X ^ sourcePower

noncomputable def EulerParentInitializedRadius.parameterSize (K Ti TiTotal Cp B δ N : ℝ) : ℝ

Parameter size, given by 1+K+Ti+TiTotal+Cp+B+δ⁻¹+N.

Equations

• EulerParentInitializedRadius.parameterSize K Ti TiTotal Cp B δ N = 1 + K + Ti + TiTotal + Cp + B + δ⁻¹ + N

theorem EulerParentInitializedRadius.parameterSize_bounds (K Ti TiTotal Cp B δ N : ℝ) (hK : 0 ≤ K) (hTi : 0 ≤ Ti) (hTiTotal : 0 ≤ TiTotal) (hCp : 0 ≤ Cp) (hB : 0 ≤ B) (hδ : 0 < δ) (hN : 0 ≤ N) : 1 ≤ parameterSize K Ti TiTotal Cp B δ N ∧ K ≤ parameterSize K Ti TiTotal Cp B δ N ∧ Ti ≤ parameterSize K Ti TiTotal Cp B δ N ∧ TiTotal ≤ parameterSize K Ti TiTotal Cp B δ N ∧ Cp ≤ parameterSize K Ti TiTotal Cp B δ N ∧ B ≤ parameterSize K Ti TiTotal Cp B δ N ∧ δ⁻¹ ≤ parameterSize K Ti TiTotal Cp B δ N ∧ N ≤ parameterSize K Ti TiTotal Cp B δ N

noncomputable def EulerParentInitializedRadius.fullEnvelope (X : ℝ) : ℝ

Full envelope, given by radiusEnvelope (sourceEnvelope X).

Equations

• EulerParentInitializedRadius.fullEnvelope X = EulerPacketRadiusPolynomial.radiusEnvelope (EulerParentInitializedRadius.sourceEnvelope X)

noncomputable def EulerParentInitializedRadius.fullPolynomial : Polynomial ℝ

Full polynomial, given by radiusPolynomial.comp (sourceRadiusPolynomial.comp inputPolynomial).

Equations

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

theorem EulerParentInitializedRadius.fullPolynomial_eval (X : ℝ) : Polynomial.eval X fullPolynomial = fullEnvelope X

noncomputable def EulerParentInitializedRadius.fullConstant : ℝ

Full constant, given by coefficientCost fullPolynomial.

Equations

• EulerParentInitializedRadius.fullConstant = EulerPolynomialCost.coefficientCost EulerParentInitializedRadius.fullPolynomial

noncomputable def EulerParentInitializedRadius.fullPower : ℕ

Full power, given by fullPolynomial.natDegree.

Equations

• EulerParentInitializedRadius.fullPower = EulerParentInitializedRadius.fullPolynomial.natDegree

theorem EulerParentInitializedRadius.fullConstant_pos : 0 < fullConstant

theorem EulerParentInitializedRadius.fullEnvelope_power (X : ℝ) (hX : 1 ≤ X) : fullEnvelope X ≤ fullConstant * X ^ fullPower

noncomputable def EulerParentPacketFrames.LabelData.canonicalInitializedRadius {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (Ti Cp : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hCp : 0 ≤ Cp) (g : C(↑(Set.Icc 0 (G.T - τ)), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 (G.T - τ))), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hphysical : EulerPacketSourcePropagator.PhysicalGrowth ((G.transverseData m hm R S hS).tail τ ⋯ hτT) EulerPacketParentPhysicalBudgets.halfBall (⇑g) Cp) (TiTotal : ℝ) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (δ : ℝ) (ξ : U) : ℝ

Canonical initialized radius, given by initializedRadius (J).mean (J).linear (J).normal BC δ ξ.

Equations

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

theorem EulerParentPacketFrames.LabelData.joined_radius_primitives {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (Ti Cp : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hCp : 0 ≤ Cp) (g : C(↑(Set.Icc 0 (G.T - τ)), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 (G.T - τ))), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hphysical : EulerPacketSourcePropagator.PhysicalGrowth ((G.transverseData m hm R S hS).tail τ ⋯ hτT) EulerPacketParentPhysicalBudgets.halfBall (⇑g) Cp) (TiTotal : ℝ) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (δ : ℝ) (ξ : U) (X : ℝ) (hKX : L.K ≤ X) (hTiX : Ti ≤ X) (hTiTotalX : TiTotal ≤ X) (hCpX : Cp ≤ X) (hLX : H.L ≤ X) (hδX : δ⁻¹ ≤ X) (hξX : ‖ξ‖ ≤ X) : EulerPacketRadiusPolynomial.RadiusPrimitives (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).mean (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).linear (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).normal (EulerPacketCylinderField.joinedCoefficientBudget EulerPacketTerminalDatum.period (G.meanData H) (G.transverseData m hm R S hS) ⋯ τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).normal) δ ξ (EulerPacketSourceRadius.sourceRadiusEnvelope (EulerParentInitializedRadius.inputEnvelope X))

theorem EulerParentPacketFrames.LabelData.canonicalInitializedRadius_power {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (Ti Cp : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hCp : 0 ≤ Cp) (g : C(↑(Set.Icc 0 (G.T - τ)), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 (G.T - τ))), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hphysical : EulerPacketSourcePropagator.PhysicalGrowth ((G.transverseData m hm R S hS).tail τ ⋯ hτT) EulerPacketParentPhysicalBudgets.halfBall (⇑g) Cp) (TiTotal : ℝ) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (X : ℝ) (hKX : L.K ≤ X) (hTiX : Ti ≤ X) (hTiTotalX : TiTotal ≤ X) (hCpX : Cp ≤ X) (hLX : H.L ≤ X) (hδX : δ⁻¹ ≤ X) (hξX : ‖ξ‖ ≤ X) : L.canonicalInitializedRadius H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal δ ξ ≤ EulerParentInitializedRadius.fullConstant * X ^ EulerParentInitializedRadius.fullPower

theorem EulerParentPacketFrames.LabelData.joined_radius_primitive_polynomial {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (Ti Cp : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hCp : 0 ≤ Cp) (g : C(↑(Set.Icc 0 (G.T - τ)), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 (G.T - τ))), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hphysical : EulerPacketSourcePropagator.PhysicalGrowth ((G.transverseData m hm R S hS).tail τ ⋯ hτT) EulerPacketParentPhysicalBudgets.halfBall (⇑g) Cp) (TiTotal : ℝ) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (δ : ℝ) (hδ : 0 < δ) (ξ : U) : have X := EulerParentInitializedRadius.parameterSize L.K Ti TiTotal Cp H.L δ ‖ξ‖; EulerPacketRadiusPolynomial.RadiusPrimitives (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).mean (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).linear (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).normal (EulerPacketCylinderField.joinedCoefficientBudget EulerPacketTerminalDatum.period (G.meanData H) (G.transverseData m hm R S hS) ⋯ τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) (L.joinedInputs H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal).normal) δ ξ (EulerParentInitializedRadius.sourceEnvelope X) ∧ EulerParentInitializedRadius.sourceEnvelope X ≤ EulerParentInitializedRadius.sourceConstant * X ^ EulerParentInitializedRadius.sourcePower

theorem EulerParentPacketFrames.LabelData.canonicalInitializedRadius_polynomial {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {G : Parent} (L : LabelData G) (H : LowBounds G) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m)) (S : Set EulerSmoothLimit.Space) (hS : IsCompact S) (τ : ℝ) (hτ : 0 < τ) (hτT : τ < G.T) (Ti Cp : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) (hCp : 0 ≤ Cp) (g : C(↑(Set.Icc 0 (G.T - τ)), ℝ)) (hg : ∀ (t : ↑(Set.Icc 0 (G.T - τ))), 0 < g t) (hg0 : g ⟨0, ⋯⟩ = 1) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : S ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hphysical : EulerPacketSourcePropagator.PhysicalGrowth ((G.transverseData m hm R S hS).tail τ ⋯ hτT) EulerPacketParentPhysicalBudgets.halfBall (⇑g) Cp) (TiTotal : ℝ) (hT1 : G.T ≤ 1) (hTiTotal : G.T⁻¹ ≤ TiTotal) (δ : ℝ) (hδ : 0 < δ) (ξ : U) : L.canonicalInitializedRadius H m hm R S hS τ hτ hτT Ti Cp hτ1 hTi hCp g hg hg0 Ω hΩ hΩo hsub hΩball hphysical TiTotal hT1 hTiTotal δ ξ ≤ EulerParentInitializedRadius.fullConstant * EulerParentInitializedRadius.parameterSize L.K Ti TiTotal Cp H.L δ ‖ξ‖ ^ EulerParentInitializedRadius.fullPower