A fixed polynomial controls the full actual neighboring-label cost, including the normal normalization and the selected terminal datum. The small label scale is kept outside this polynomial.

def EulerParentNeighborCost.formula (F V R Hist Ei Hi CM CH : ℝ) : ℝ

Formula, given by 27*F^2*V*R+27*F^2*R*(1+F)*Ei + 16*Hist*(5+64*CM^2+2*CH)*(1+3*F^2)*Hi*Ei.

Equations

• EulerParentNeighborCost.formula F V R Hist Ei Hi CM CH = 27 * F ^ 2 * V * R + 27 * F ^ 2 * R * (1 + F) * Ei + 16 * Hist * (5 + 64 * CM ^ 2 + 2 * CH) * (1 + 3 * F ^ 2) * Hi * Ei

noncomputable def EulerParentNeighborCost.envelope (K Ti Ei Hi CM CH : ℝ) : ℝ

Envelope, constructed using formula.

Equations

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

noncomputable def EulerParentNeighborCost.polynomial : Polynomial ℝ

Polynomial as an element of Polynomial ℝ.

Equations

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

noncomputable def EulerParentNeighborCost.boundConstant : ℝ

Bound constant, given by coefficientCost polynomial.

Equations

• EulerParentNeighborCost.boundConstant = EulerPolynomialCost.coefficientCost EulerParentNeighborCost.polynomial

noncomputable def EulerParentNeighborCost.degree : ℕ

Degree, given by polynomial.natDegree.

Equations

• EulerParentNeighborCost.degree = EulerParentNeighborCost.polynomial.natDegree

theorem EulerParentNeighborCost.constant_pos : 0 < boundConstant

theorem EulerParentNeighborCost.polynomial_eval (P : ℝ) : Polynomial.eval P polynomial = formula (EulerPacketParentLabelBounds.frameAmplitude P) (EulerPacketParentLabelBounds.gradientAmplitude P) (1024 + 4 * P) (EulerParentHistoryCost.labelHistoryConstant * P ^ EulerParentHistoryCost.labelHistoryPower) P P P P

theorem EulerParentNeighborCost.formula_mono {F V R Hist Ei Hi CM CH F' V' R' Hist' Ei' Hi' CM' CH' : ℝ} (hF : 0 ≤ F) (hV : 0 ≤ V) (hR : 0 ≤ R) (hHist : 0 ≤ Hist) (hEi : 0 ≤ Ei) (hHi : 0 ≤ Hi) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) (hFF : F ≤ F') (hVV : V ≤ V') (hRR : R ≤ R') (hHH : Hist ≤ Hist') (hEE : Ei ≤ Ei') (hII : Hi ≤ Hi') (hMM : CM ≤ CM') (hCC : CH ≤ CH') : formula F V R Hist Ei Hi CM CH ≤ formula F' V' R' Hist' Ei' Hi' CM' CH'

theorem EulerParentNeighborCost.envelope_power (K Ti Ei Hi CM CH : ℝ) (hK : 0 ≤ K) (hTi : 0 ≤ Ti) (hEi : 0 ≤ Ei) (hHi : 0 ≤ Hi) (hCM : 0 ≤ CM) (hCH : 0 ≤ CH) : envelope K Ti Ei Hi CM CH ≤ boundConstant * (1 + K + Ti + Ei + Hi + CM + CH) ^ degree

theorem EulerPacketSourceGeometry.ParentFrame.epsilon_inv_le_twice_shear {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] {D : EulerTransversePacketProvider.Data U} {τ : ℝ} (P : ParentFrame D τ) (ha : 1 / 2 ≤ P.a) (hH : 1 ≤ P.shear) : P.epsilon⁻¹ ≤ 2 * P.shear

theorem EulerParentPacketFrames.LabelData.neighborScaleCost_envelope {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) (hCH : 0 ≤ CH) (hshear : 0 < P.shear) (heps : 0 < P.epsilon) : L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH ≤ EulerParentNeighborCost.envelope L.K Ti P.epsilon⁻¹ P.shear⁻¹ CM CH

theorem EulerParentPacketFrames.LabelData.neighborScaleCost_polynomial {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) (hshear : 0 < P.shear) (heps : 0 < P.epsilon) : L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH ≤ EulerParentNeighborCost.boundConstant * (1 + L.K + Ti + P.epsilon⁻¹ + P.shear⁻¹ + CM + CH) ^ EulerParentNeighborCost.degree

theorem EulerParentPacketFrames.LabelData.source_neighbor_polynomial {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) (hshear : 0 < P.shear) (heps : 0 < P.epsilon) : P.neighborCost hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) CM CH ≤ EulerParentNeighborCost.boundConstant * (1 + L.K + Ti + P.epsilon⁻¹ + P.shear⁻¹ + CM + CH) ^ EulerParentNeighborCost.degree * G.ell

theorem EulerParentPacketFrames.LabelData.neighborScaleCost_low_polynomial {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) : L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH ≤ EulerParentNeighborCost.boundConstant * (2 * (1 + CM + CH)) ^ EulerParentNeighborCost.degree * (1 + L.K + Ti + P.shear) ^ EulerParentNeighborCost.degree

With the actual activation scales, only the positive shear itself is needed as a polynomial variable. CM and CH remain fixed low constants.

theorem EulerParentPacketFrames.LabelData.source_neighbor_low_polynomial {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) : P.neighborCost hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) CM CH ≤ EulerParentNeighborCost.boundConstant * (2 * (1 + CM + CH)) ^ EulerParentNeighborCost.degree * (1 + L.K + Ti + P.shear) ^ EulerParentNeighborCost.degree * G.ell