The actual zero-history geometry constructs the forward packet and its new smooth Euler state at the uniformly chosen frequency.

structure EulerParentPacketFrames.GeometryForwardInput (U : Type) [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] : Type

Geometry forward input data, collecting parent, label, low, normal, normal_unit, coordinates and their compatibility conditions.

• parent : Parent

  Parent of GeometryForwardInput, of type Parent.

• label : LabelData self.parent

  Label of GeometryForwardInput, of type LabelData parent.

• low : LowBounds self.parent

  Low of GeometryForwardInput, of type LowBounds parent.

• normal : EulerSmoothLimit.Space

  Normal of GeometryForwardInput, of type Space.

• normal_unit : ‖self.normal‖ = 1
• coordinates : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane self.normal)

  Coordinates of GeometryForwardInput, of type U ≃ₗᵢ[ℝ] EulerTransverseFrameCoordinates.referencePlane normal.

• support : Set EulerSmoothLimit.Space

  Support set of GeometryForwardInput, of type Set Space.

• support_compact : IsCompact self.support
• total_le_one : self.parent.T ≤ 1
• frame : EulerPacketSourceGeometry.ParentFrame (self.parent.transverseData self.normal ⋯ self.coordinates self.support ⋯) 0

  Frame of GeometryForwardInput, of type ParentFrame (parent.transverseData normal normal_unit coordinates support support_compact) 0.

• geometry : EulerPacketSourceGeometry.ForwardGuards self.frame

  Geometry of GeometryForwardInput, of type ForwardGuards frame.

• halfBall : 1 / 2 ≤ self.geometry.radius
• neighborhood : Set EulerSmoothLimit.Space

  Neighborhood of GeometryForwardInput, of type Set Space.

• neighborhood_measurable : MeasurableSet self.neighborhood
• neighborhood_open : IsOpen self.neighborhood
• support_subset : self.support ⊆ self.neighborhood
• neighborhood_bound (x : EulerSmoothLimit.Space) : x ∈ self.neighborhood → ‖x‖ ≤ 1 / 2
• cutoff_support : tsupport EulerSpatialCutoffs.innerCutoff ⊆ self.support
• delta_pos : 0 < self.geometry.δ
• delta_le_one : self.geometry.δ ≤ 1
• child_pos : 0 < self.geometry.hchild

@[reducible, inline]

noncomputable abbrev EulerParentPacketFrames.GeometryForwardInput.data {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) : EulerTransversePacketProvider.Data U

Data: an abbreviation for I.parent.transverseData I.normal I.normal_unit I.coordinates I.support I.support_compact.

Equations

• I.data = I.parent.transverseData I.normal ⋯ I.coordinates I.support ⋯

@[reducible, inline]

noncomputable abbrev EulerParentPacketFrames.GeometryForwardInput.meanData {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) : EulerMeanPacketProvider.Data

Mean data: an abbreviation for I.parent.meanData I.low.

Equations

• I.meanData = I.parent.meanData I.low

@[reducible, inline]

abbrev EulerParentPacketFrames.GeometryForwardInput.agreement {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) : EulerPacketCylinderField.SourceCoefficientAgreement I.meanData I.data

Agreement: an abbreviation for I.parent.sourceAgreement I.normal I.normal_unit I.coordinates I.support I.support_compact I.low.

Equations

• ⋯ = ⋯

noncomputable def EulerParentPacketFrames.GeometryForwardInput.parameterSize {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) : ℝ

Parameter size, constructed using I.label.geometryForwardParameterSize.

Equations

• I.parameterSize = I.label.geometryForwardParameterSize I.low I.normal ⋯ I.coordinates I.support ⋯ I.frame I.geometry I.parent.T⁻¹ I.geometry.initialCoordinate

noncomputable def EulerParentPacketFrames.GeometryForwardInput.alpha {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) : ℝ

Alpha, given by I.geometry.primaryAmplitude I.halfBall.

Equations

• I.alpha = I.geometry.primaryAmplitude ⋯

theorem EulerParentPacketFrames.GeometryForwardInput.alpha_pos {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) : 0 < I.alpha

def EulerParentPacketFrames.GeometryForwardInput.frequencyGuard {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (k : ℝ) : Prop

Frequency guard, given by frequencyConstant*I.parameterSize^frequencyPower ≤ smallPower k.

Equations

• I.frequencyGuard k = (EulerPacketUniformSource.frequencyConstant * I.parameterSize ^ EulerPacketUniformSource.frequencyPower ≤ EulerPacketSourceFrequency.smallPower k)

@[reducible, inline]

abbrev EulerParentPacketFrames.GeometryForwardInput.correctionBudget {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (k : ℝ) (hk : 4 ≤ k) (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) : Type

Correction budget type used in parent geometry forward choice.

Equations

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

structure EulerParentPacketFrames.GeometryForwardChoice {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) : Type

Geometry forward choice data, collecting hn, Q, flow, graph, coefficient, labels and their compatibility conditions.

• hn : 1 ≤ EulerPacketSourceFrequency.truncation k
• Q : I.correctionBudget k ⋯ ⋯

  Scale parameter of GeometryForwardChoice, of type I.correctionBudget k hk.four hn.

• flow : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period I.parent.T

  Flow of GeometryForwardChoice, of type EulerPhysicalGraphFlowBounds.Data period I.parent.T.

• graph (t : ↑(Set.Icc 0 I.parent.T)) (q : EulerLiftedGradientSpace.LiftTangent) : (EulerGraphInvariantFlow.graphConstraint k I.normal) ((self.flow.A.field t) q) = 0
• coefficient : self.flow.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period self.Q (EulerPacketTerminalDatum.forwardInitializedNormalizedField I.meanData I.data ⋯ I.geometry.δ ⋯ I.geometry.initialCoordinate ⋯ I.alpha (EulerPacketSourceFrequency.truncation k) k)
• labels : LabelData (I.parent.child self.flow k I.normal ⋯ nextEll hnext hnext1)

  Label type of GeometryForwardChoice, of type LabelData (I.parent.child flow k I.normal graph nextEll hnext hnext1).

• label_constant : self.labels.K = k ^ 80
• displacement_bound (t : ↑(Set.Icc 0 I.parent.T)) (x : EulerSmoothLimit.Space) : ‖(self.flow.displacementField k I.normal I.parent.ell ⋯ t).field x‖ ≤ k ^ (-(1 / 4))
• errors : S.evolution.ForwardSourceErrors I.normal ⋯ I.coordinates I.support ⋯ self.Q (EulerPacketTerminalDatum.forwardInitializedApproximationResidual I.meanData I.data ⋯ I.geometry.δ ⋯ I.geometry.initialCoordinate ⋯ I.alpha ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯) k I.geometry ⋯ (k ^ (-(1 / 4))) (k ^ (-(1 / 4)))

theorem EulerParentPacketFrames.exists_geometryForwardChoice {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (hfrequency : I.frequencyGuard k) (hK : I.label.K ≤ k) (hell : I.parent.ell⁻¹ ≤ k ^ (3 / 4)) : Nonempty (GeometryForwardChoice I S k hk nextEll hnext hnext1)

noncomputable def EulerParentPacketFrames.GeometryForwardChoice.parent {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) : Parent

Parent, given by I.parent.child F.flow k I.normal F.graph nextEll hnext hnext1.

Equations

• EulerParentPacketFrames.GeometryForwardChoice.parent I S k hk nextEll hnext hnext1 F = I.parent.child F.flow k I.normal ⋯ nextEll hnext hnext1

noncomputable def EulerParentPacketFrames.GeometryForwardChoice.state {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) : SmoothState (parent I S k hk nextEll hnext hnext1 F)

State, constructed using S.forwardChild.

Equations

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

theorem EulerParentPacketFrames.GeometryForwardChoice.state_label_constant {U : Type} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (I : GeometryForwardInput U) (S : SmoothState I.parent) (k : ℝ) (hk : EulerPacketSourceFrequency.UniversalFrequency k) (nextEll : ℝ) (hnext : 0 < nextEll) (hnext1 : nextEll ≤ 1) (F : GeometryForwardChoice I S k hk nextEll hnext hnext1) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support) : (state I S k hk nextEll hnext hnext1 F hSym).labels.K = k ^ 80