Concrete support, transverse coordinate and short-time source budgets for the first packet over the compact base Euler solution.

The concrete compactly supported datum supplies the full recursive state: the physical Euler solution, all Sobolev orders, particle labels, and odd symmetry all refer to the same solution.

noncomputable def EulerBaseDatum.initialState (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) : EulerParentPacketFrames.SmoothState (initialParent β hβ ell hell hell1)

Initial state, bundling evolution, regularity, labels, odd.

Equations

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

def EulerPacketSupport.support : Set EulerSmoothLimit.Space

Support, given by tsupport innerCutoff.

Equations

• EulerPacketSupport.support = tsupport EulerSpatialCutoffs.innerCutoff

theorem EulerPacketSupport.compact : IsCompact support

theorem EulerPacketSupport.subset_halfBall : support ⊆ Metric.ball 0 (1 / 2)

theorem EulerPacketSupport.symmetric (x : EulerSmoothLimit.Space) : -x ∈ support ↔ x ∈ support

theorem EulerPacketSupport.norm_lt (x : EulerSmoothLimit.Space) (hx : x ∈ support) : ‖x‖ < 1 / 2

noncomputable def EulerBaseDatum.firstNormal : EulerSmoothLimit.Space

First normal, given by EuclideanSpace.single 0 1.

Equations

• EulerBaseDatum.firstNormal = EuclideanSpace.single 0 1

theorem EulerBaseDatum.firstNormal_unit : ‖firstNormal‖ = 1

@[reducible, inline]

noncomputable abbrev EulerBaseDatum.FirstPlane : Submodule ℝ EulerSmoothLimit.Space

First plane: an abbreviation for referencePlane firstNormal.

Equations

• EulerBaseDatum.FirstPlane = EulerTransverseFrameCoordinates.referencePlane EulerBaseDatum.firstNormal

noncomputable def EulerBaseDatum.firstFrame : ↥FirstPlane ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane firstNormal)

First frame, given by LinearIsometryEquiv.refl ℝ _.

Equations

• EulerBaseDatum.firstFrame = LinearIsometryEquiv.refl ℝ ↥EulerBaseDatum.FirstPlane

noncomputable def EulerBaseDatum.firstCoordinate : ↥FirstPlane

First coordinate as an element of FirstPlane.

Equations

• EulerBaseDatum.firstCoordinate = ⟨EuclideanSpace.single 1 1, EulerBaseDatum.firstCoordinate._proof_2⟩

theorem EulerBaseDatum.firstCoordinate_map : ↑(firstFrame firstCoordinate) = EuclideanSpace.single 1 1

theorem EulerBaseDatum.firstCoordinate_norm : ‖firstCoordinate‖ = 1

noncomputable def EulerBaseDatum.packetBaseParent (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : EulerParentPacketFrames.Parent

Packet base parent, given by (initialParent β hβ ell hell hell1).restrictTime T hT hTB.

Equations

• EulerBaseDatum.packetBaseParent β hβ ell hell hell1 T hT hTB = (EulerBaseDatum.initialParent β hβ ell hell hell1).restrictTime T hT hTB

noncomputable def EulerBaseDatum.packetBaseState (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : EulerParentPacketFrames.SmoothState (packetBaseParent β hβ ell hell hell1 T hT hTB)

Packet base state, given by (initialState β hβ ell hell hell1).restrictTime T hT hTB.

Equations

• EulerBaseDatum.packetBaseState β hβ ell hell hell1 T hT hTB = (EulerBaseDatum.initialState β hβ ell hell hell1).restrictTime T hT hTB

noncomputable def EulerBaseDatum.packetBaseLowBounds (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : EulerParentPacketFrames.LowBounds (packetBaseParent β hβ ell hell hell1 T hT hTB)

Packet base low bounds, given by (initialLowBounds β hβ ell hell hell1).restrictTime T hT hTB.

Equations

• EulerBaseDatum.packetBaseLowBounds β hβ ell hell hell1 T hT hTB = (EulerBaseDatum.initialLowBounds β hβ ell hell hell1).restrictTime T hT hTB

theorem EulerBaseDatum.packetBase_label_constant (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseState β hβ ell hell hell1 T hT hTB).labels.K = solutionLabelConstant

theorem EulerBaseDatum.packetBase_boundary_zero (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (packetBaseLowBounds β hβ ell hell hell1 T hT hTB).L = 0

theorem EulerBaseDatum.packetBase_short (T : ℝ) (hTB : T ≤ initialTime) : initialCoefficientCost * T ≤ 1 / 2

theorem EulerBaseDatum.packetBase_sign_short (T : ℝ) (hTB : T ≤ initialTime) : EulerPacketFirstPressureSign.firstSignRate initialCoefficientCost initialCoefficientCost * T ≤ 1 / 2

theorem EulerBaseDatum.packetBase_strain_bound (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖((packetBaseParent β hβ ell hell hell1 T hT hTB).strain.field t) x‖ ≤ initialCoefficientCost

theorem EulerBaseDatum.packetBase_curvature_bound (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖((packetBaseParent β hβ ell hell hell1 T hT hTB).curvature.field t) x‖ ≤ initialCoefficientCost

theorem EulerBaseDatum.packetBase_initialStrain (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (x : EulerSmoothLimit.Space) (hx : x ∈ EulerPacketSupport.support) : (packetBaseParent β hβ ell hell hell1 T hT hTB).initialStrain.field x = linear β

noncomputable def EulerBaseDatum.firstPacketInputs (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : EulerParentPacketFrames.ForwardInputs ((packetBaseParent β hβ ell hell hell1 T hT hTB).meanData (packetBaseLowBounds β hβ ell hell hell1 T hT hTB)) ((packetBaseParent β hβ ell hell hell1 T hT hTB).transverseData firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact)

First packet inputs used in base packet setup.

Equations

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

theorem EulerBaseDatum.firstPacketInputs_growth (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) : (firstPacketInputs β hβ ell hell hell1 T hT hTB).linear.g = 1

theorem EulerBaseDatum.firstPacket_pressure_numerator (β : ℝ) (hβ : |β| ≤ 1) (ell : ℝ) (hell : 0 < ell) (hell1 : ell ≤ 1) (T : ℝ) (hT : 0 < T) (hTB : T ≤ initialTime) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (hx : x ∈ EulerPacketSupport.support) : 1 / 2 ≤ inner ℝ ((((packetBaseParent β hβ ell hell hell1 T hT hTB).transverseData firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact).normal.field t) x) ((((packetBaseParent β hβ ell hell hell1 T hT hTB).strain.field t) x) (EulerPacketForwardFactorization.uncutVelocity ((packetBaseParent β hβ ell hell hell1 T hT hTB).transverseData firstNormal firstNormal_unit firstFrame EulerPacketSupport.support EulerPacketSupport.compact) firstCoordinate (↑t) x))