The actual restricted history sensitivity has a single fixed polynomial dependence on the parent label constant and reciprocal history length. The small physical scale remains a multiplicative factor.

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketHistoryPolynomial1 {V : Type} [NormedAddCommGroup V] : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedAddCommGroup (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketHistoryPolynomial1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketHistoryPolynomial2 {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space V)

Cache the standard NormedSpace ℝ (Space →ᵇ V) instance to shorten typeclass synthesis.

Equations

• EulerMeanCoefficients.SmoothCoefficientPath.instParentPacketHistoryPolynomial2 = inferInstance

theorem EulerMeanCoefficients.SmoothCoefficientPath.field_norm_le_of_bound {J V : Type} [TopologicalSpace J] [CompactSpace J] [NormedAddCommGroup V] [NormedSpace ℝ V] (A : SmoothCoefficientPath J V) (C : ℝ) (hC : 0 ≤ C) (hb : ∀ (t : J) (x : EulerSmoothLimit.Space), ‖(A.field t) x‖ ≤ C) : ‖A.field‖ ≤ C

theorem EulerTransversePacketProvider.Data.frame_norm_le {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (C : ℝ) (hC : 0 ≤ C) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) : ‖D.frame.field‖ ≤ C

theorem EulerTransversePacketProvider.Data.frameDerivative_norm_le {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (C1 : ℝ) (hC1 : 0 ≤ C1) (hF1 : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F₁.field t) x‖ ≤ C1) : ‖D.frameDerivative.field‖ ≤ C1

theorem EulerParentPacketFrames.LabelData.initialHistoryDifferenceScaleCost_bound {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) (Ti : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) : L.initialHistoryDifferenceScaleCost m hm R S hS H τ hτ hτT ≤ EulerParentHistoryCost.labelHistoryEnvelope L.K Ti

theorem EulerParentPacketFrames.LabelData.initial_history_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) (Ti : ℝ) (hτ1 : τ ≤ 1) (hTi : τ⁻¹ ≤ Ti) : EulerPacketActivationHistory.historyLabelDifferenceCost (G.historyOn H m hm R S hS τ hτ hτT) ≤ EulerParentHistoryCost.labelHistoryConstant * (1 + L.K + Ti) ^ EulerParentHistoryCost.labelHistoryPower * G.ell