The chosen geometric profile contributes only another fixed polynomial in the source primitives, including the target shear.

noncomputable def EulerPacketUniformSource.profileEnvelope (X : ℝ) : ℝ

Profile envelope, given by 1+sourceEnvelope X+8*Real.exp 6*X*(1+sourceEnvelope X).

Equations

• EulerPacketUniformSource.profileEnvelope X = 1 + EulerParentInitializedRadius.sourceEnvelope X + 8 * Real.exp 6 * X * (1 + EulerParentInitializedRadius.sourceEnvelope X)

noncomputable def EulerPacketUniformSource.profilePolynomial : Polynomial ℝ

Profile polynomial, given by 1+sourcePolynomial+Polynomial.C (8*Real.exp 6)*Polynomial.X*(1+sourcePolynomial).

Equations

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

theorem EulerPacketUniformSource.profilePolynomial_eval (X : ℝ) : Polynomial.eval X profilePolynomial = profileEnvelope X

theorem EulerPacketUniformSource.sourceEnvelope_one (X : ℝ) (hX : 1 ≤ X) : 1 ≤ EulerParentInitializedRadius.sourceEnvelope X

theorem EulerPacketUniformSource.profileEnvelope_bounds (X : ℝ) (hX : 1 ≤ X) : 1 ≤ profileEnvelope X ∧ EulerParentInitializedRadius.sourceEnvelope X ≤ profileEnvelope X ∧ 8 * Real.exp 6 * X * (1 + EulerParentInitializedRadius.sourceEnvelope X) ≤ profileEnvelope X

theorem EulerPacketUniformSource.profile_amplitude_le (X δ h C : ℝ) (hX : 1 ≤ X) (_hδ : 0 ≤ δ) (hδ1 : δ ≤ 1) (hh : 0 ≤ h) (hhX : h ≤ X) (hC : 0 ≤ C) (hCS : C ≤ EulerParentInitializedRadius.sourceEnvelope X) : 8 * Real.exp 6 * δ * h * (1 + C) ≤ profileEnvelope X

noncomputable def EulerPacketUniformSource.frequencyPolynomial : Polynomial ℝ

Frequency polynomial, given by Polynomial.C EulerPacketInitializedOutputCost.uniformConstant * profilePolynomial^EulerPacketInitializedOutputCost.uniformPower.

noncomputable def EulerPacketUniformSource.frequencyConstant : ℝ

Frequency constant, given by coefficientCost frequencyPolynomial.

Equations

• EulerPacketUniformSource.frequencyConstant = EulerPolynomialCost.coefficientCost EulerPacketUniformSource.frequencyPolynomial

noncomputable def EulerPacketUniformSource.frequencyPower : ℕ

Frequency power, given by frequencyPolynomial.natDegree.

Equations

• EulerPacketUniformSource.frequencyPower = EulerPacketUniformSource.frequencyPolynomial.natDegree

theorem EulerPacketUniformSource.frequencyConstant_pos : 0 < frequencyConstant

theorem EulerPacketUniformSource.frequencyPolynomial_eval (X : ℝ) : Polynomial.eval X frequencyPolynomial = EulerPacketInitializedOutputCost.uniformConstant * profileEnvelope X ^ EulerPacketInitializedOutputCost.uniformPower

theorem EulerPacketUniformSource.frequency_bound (X : ℝ) (hX : 1 ≤ X) : EulerPacketInitializedOutputCost.uniformConstant * profileEnvelope X ^ EulerPacketInitializedOutputCost.uniformPower ≤ frequencyConstant * X ^ frequencyPower

theorem EulerPacketSourceGeometry.Guards.source_uniform_primitives {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} {hτ : 0 < τ} {hτT : τ < D.T} {P : ParentFrame D τ} {H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)} (J : Guards hτ hτT P H) (hball : 1 / 2 ≤ J.radius) (L : EulerTransversePacketJoin.Budget D τ hτ hτT H (Fin 4) 6) (hg : L.g = J.sourceGrowthProfile hball) {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (ξ : U) (X : ℝ) (hX : 1 ≤ X) (hhX : J.hchild ≤ X) (hδ1 : J.δ ≤ 1) (hR : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB BC J.δ ξ (EulerParentInitializedRadius.sourceEnvelope X)) : EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB BC J.δ ξ (EulerPacketUniformSource.profileEnvelope X) ∧ ∀ (t : ↑(Set.Icc 0 D.T)), J.primaryAmplitude hball * L.fullProfile t ≤ EulerPacketUniformSource.profileEnvelope X

theorem EulerPacketForwardRadius.RadiusPrimitives.mono {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {L : EulerTransversePacketForward.Budget D (Fin 4) 6} {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} {LM : EulerMeanPacketProvider.Budget M 6 Rm} {NB : EulerTransversePacketJoin.NormalBudget D 6 L.R} {BC : EulerPacketCylinderField.CoefficientBudget C} {δ : ℝ} {ξ : U} {X Y : ℝ} (H : RadiusPrimitives L LM NB BC δ ξ X) (hXY : X ≤ Y) : RadiusPrimitives L LM NB BC δ ξ Y

theorem EulerPacketSourceGeometry.ForwardGuards.source_uniform_primitives {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] {D : EulerTransversePacketProvider.Data U} {P : ParentFrame D 0} (J : ForwardGuards P) (hball : 1 / 2 ≤ J.radius) (L : EulerTransversePacketForward.Budget D (Fin 4) 6) (hg : L.g = J.sourceGrowthProfile hball) {M : EulerMeanPacketProvider.Data} {Rm Tc : ℝ} {O : EulerPacketProfileRecursion.Operators} {C : EulerPacketCylinderField.CoefficientData EulerPacketTerminalDatum.period Tc O} (LM : EulerMeanPacketProvider.Budget M 6 Rm) (NB : EulerTransversePacketJoin.NormalBudget D 6 L.R) (BC : EulerPacketCylinderField.CoefficientBudget C) (ξ : U) (X : ℝ) (hX : 1 ≤ X) (hhX : J.hchild ≤ X) (hδ1 : J.δ ≤ 1) (hR : EulerPacketForwardRadius.RadiusPrimitives L LM NB BC J.δ ξ (EulerParentInitializedRadius.sourceEnvelope X)) : EulerPacketForwardRadius.RadiusPrimitives L LM NB BC J.δ ξ (EulerPacketUniformSource.profileEnvelope X) ∧ ∀ (t : ↑(Set.Icc 0 D.T)), J.primaryAmplitude hball * L.g t ≤ EulerPacketUniformSource.profileEnvelope X