The literal compact terminal datum χ₁(y) fδ(θ) ξT. The periodic variable has period 2π. The constant vector is multiplied by the spatial cutoff before it is placed in the genuine cylinder L² space.

@[reducible, inline]

noncomputable abbrev EulerPacketTerminalDatum.period : ℝ

Period: an abbreviation for 2 * Real.pi.

Equations

• EulerPacketTerminalDatum.period = 2 * Real.pi

instance EulerPacketTerminalDatum.period_pos : Fact (0 < period)

noncomputable def EulerPacketTerminalDatum.scalarField (δ : ℝ) (x : EulerLiftedGradientSpace.LiftDomain period) : ℝ

Scalar field, given by innerCutoff x.1 * (profile_periodic δ).lift x.2.

Equations

• EulerPacketTerminalDatum.scalarField δ x = EulerSpatialCutoffs.innerCutoff x.1 * ⋯.lift x.2

noncomputable def EulerPacketTerminalDatum.field {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (ξ : U) (x : EulerLiftedGradientSpace.LiftDomain period) : U

Field, given by scalarField δ x • ξ.

Equations

• EulerPacketTerminalDatum.field δ ξ x = EulerPacketTerminalDatum.scalarField δ x • ξ

@[simp]

theorem EulerPacketTerminalDatum.scalarField_coe (δ : ℝ) (y : EulerSmoothLimit.Space) (θ : ℝ) : scalarField δ (y, ↑θ) = EulerSpatialCutoffs.innerCutoff y * EulerPeriodicProfile.profile δ θ

@[simp]

theorem EulerPacketTerminalDatum.field_coe {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (ξ : U) (y : EulerSmoothLimit.Space) (θ : ℝ) : field δ ξ (y, ↑θ) = (EulerSpatialCutoffs.innerCutoff y * EulerPeriodicProfile.profile δ θ) • ξ

theorem EulerPacketTerminalDatum.local_scalarField (δ : ℝ) (y : EulerSmoothLimit.Space) (θ : ℝ) : EulerMetricTransport.localFieldLift period (scalarField δ) (y, ↑θ) = fun (a : EulerLiftedGradientSpace.LiftTangent) => EulerSpatialCutoffs.innerCutoff (y + a.1) * EulerPeriodicProfile.profile δ (θ + a.2)

theorem EulerPacketTerminalDatum.scalarField_smooth (δ : ℝ) (hδ : 0 < δ) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (scalarField δ) x)

theorem EulerPacketTerminalDatum.field_smooth {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (field δ ξ) x)

def EulerPacketTerminalDatum.supportSet : Set (EulerLiftedGradientSpace.LiftDomain period)

Support set, given by tsupport innerCutoff ×ˢ Set.univ.

Equations

• EulerPacketTerminalDatum.supportSet = tsupport EulerSpatialCutoffs.innerCutoff ×ˢ Set.univ

theorem EulerPacketTerminalDatum.supportSet_compact : IsCompact supportSet

theorem EulerPacketTerminalDatum.field_zero_outside {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (ξ : U) (x : EulerLiftedGradientSpace.LiftDomain period) (hx : x.1 ∉ tsupport EulerSpatialCutoffs.innerCutoff) : field δ ξ x = 0

theorem EulerPacketTerminalDatum.field_support {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (ξ : U) : tsupport (field δ ξ) ⊆ supportSet

theorem EulerPacketTerminalDatum.field_compact {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (ξ : U) : HasCompactSupport (field δ ξ)

noncomputable def EulerPacketTerminalDatum.compactField {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) : EulerCylinderCompact.CompactField period U

Compact field, bundling field, compact, smooth.

Equations

• EulerPacketTerminalDatum.compactField δ hδ ξ = { field := EulerPacketTerminalDatum.field δ ξ, compact := ⋯, smooth := ⋯ }

noncomputable def EulerPacketTerminalDatum.terminal {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) : ↥(EulerLpCylinderTranslation.CylinderL2 period U)

Terminal, given by (compactField δ hδ ξ).toLp.

Equations

• EulerPacketTerminalDatum.terminal δ hδ ξ = (EulerPacketTerminalDatum.compactField δ hδ ξ).toLp

theorem EulerPacketTerminalDatum.terminal_ae {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) : ↑↑(terminal δ hδ ξ) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] field δ ξ

theorem EulerPacketTerminalDatum.terminal_orbit_contDiff {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (ξ : U) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period a) (terminal δ hδ ξ)

theorem EulerPacketTerminalDatum.field_odd {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (ξ : U) (x : EulerLiftedGradientSpace.LiftDomain period) : field δ ξ (-x) = -field δ ξ x

theorem EulerPacketTerminalDatum.profile_integral_zero (δ : ℝ) : ∫ (θ : ℝ) in 0..period, EulerPeriodicProfile.profile δ θ = 0

theorem EulerPacketTerminalDatum.field_integral_zero {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] [CompleteSpace U] (δ : ℝ) (ξ : U) (y : EulerSmoothLimit.Space) : ∫ (θ : ℝ) in 0..period, field δ ξ (y, ↑θ) = 0