Actual mixed L² and fixed-Hq bounds for χ₁(y) fδ(θ) ξT. All constants are explicit: the only support factor is the fixed L² mass of the cutoff support cylinder. The one-time conversion from tensor jets to words precedes the fixed-radius linear solves.

True mixed L² derivative bounds for compact smooth cylinder data. One fixed compact support set supplies the L² mass factor at every order. The conversion to fixed-Hq word sums is performed once on the initial datum, before any same-radius inverse estimate is applied.

noncomputable def EulerCylinderCompact.supportMass (P : ℝ) [Fact (0 < P)] (K : Set (EulerLiftedGradientSpace.LiftDomain P)) (hK : IsCompact K) : ℝ

Support mass, given by ‖(indicatorConstLp 2 hK.isClosed.measurableSet hK.measure_ne_top (1 : ℝ) : Lp ℝ 2 (liftMeasure P))‖.

Equations

• EulerCylinderCompact.supportMass P K hK = ‖MeasureTheory.indicatorConstLp 2 ⋯ ⋯ 1‖

theorem EulerCylinderCompact.CompactField.derivative_support {P : ℝ} {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) : tsupport A.derivative.field ⊆ tsupport A.field

theorem EulerCylinderCompact.CompactField.toLp_norm_le {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) (K : Set (EulerLiftedGradientSpace.LiftDomain P)) (hK : IsCompact K) (hs : tsupport A.field ⊆ K) (C : ℝ) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ‖A.field x‖ ≤ C) : ‖A.toLp‖ ≤ C * supportMass P K hK

theorem EulerCylinderCompact.CompactField.norm_iteratedFDeriv_translation_le {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) (K : Set (EulerLiftedGradientSpace.LiftDomain P)) (hK : IsCompact K) (hs : tsupport A.field ⊆ K) (n : ℕ) (C : ℝ) (hb : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), ‖iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P A.field x) 0‖ ≤ C) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P b) A.toLp) a‖ ≤ C * supportMass P K hK

theorem EulerCylinderCompact.CompactField.translation_gevrey {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] (A : CompactField P V) (K : Set (EulerLiftedGradientSpace.LiftDomain P)) (hK : IsCompact K) (hs : tsupport A.field ⊆ K) (R C : ℝ) (hb : ∀ (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain P), ‖iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P A.field x) 0‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P b) A.toLp) a‖ ≤ C * supportMass P K hK * EulerGevrey.majorant R 0 n

theorem EulerCylinderCompact.CompactField.translation_block_bound {P : ℝ} [Fact (0 < P)] {V : Type u} [NormedAddCommGroup V] [NormedSpace ℝ V] {ι : Type u_1} [Fintype ι] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (A : CompactField P V) (K : Set (EulerLiftedGradientSpace.LiftDomain P)) (hK : IsCompact K) (hs : tsupport A.field ⊆ K) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hb : ∀ (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain P), ‖iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift P A.field x) 0‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P b) A.toLp) n a ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q R (C * supportMass P K hK) * EulerGevrey.majorant (EulerParameterWordGevrey.sobolevCoefficientRadius ι R) 0 n

noncomputable def EulerPacketTerminalDatum.jetRadius (δ : ℝ) : ℝ

Jet radius, given by 64 + 40 * (δ^2)⁻¹.

Equations

• EulerPacketTerminalDatum.jetRadius δ = 64 + 40 * (δ ^ 2)⁻¹

noncomputable def EulerPacketTerminalDatum.scalarJetCost (δ : ℝ) : ℝ

Scalar jet cost, given by 3 * (9 / rawBump 0)^3 * (100 * (δ^2)⁻¹).

Equations

• EulerPacketTerminalDatum.scalarJetCost δ = 3 * (9 / EulerGevreyCutoff.rawBump 0) ^ 3 * (100 * (δ ^ 2)⁻¹)

theorem EulerPacketTerminalDatum.jetRadius_nonneg (δ : ℝ) : 0 ≤ jetRadius δ

theorem EulerPacketTerminalDatum.scalarJetCost_nonneg (δ : ℝ) : 0 ≤ scalarJetCost δ

theorem EulerPacketTerminalDatum.scalarField_jet_bound (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift period (scalarField δ) x) a‖ ≤ scalarJetCost δ * EulerGevrey.majorant (jetRadius δ) 0 n

theorem EulerPacketTerminalDatum.field_jet_bound {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (ξ : U) (n : ℕ) (x : EulerLiftedGradientSpace.LiftDomain period) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (EulerMetricTransport.localFieldLift period (field δ ξ) x) a‖ ≤ scalarJetCost δ * ‖ξ‖ * EulerGevrey.majorant (jetRadius δ) 0 n

noncomputable def EulerPacketTerminalDatum.terminalMass : ℝ

Terminal mass, given by supportMass period supportSet supportSet_compact.

Equations

• EulerPacketTerminalDatum.terminalMass = EulerCylinderCompact.supportMass EulerPacketTerminalDatum.period EulerPacketTerminalDatum.supportSet EulerPacketTerminalDatum.supportSet_compact

theorem EulerPacketTerminalDatum.terminalMass_nonneg : 0 ≤ terminalMass

theorem EulerPacketTerminalDatum.terminal_jet_bound {U : Type u_1} [NormedAddCommGroup U] [NormedSpace ℝ U] (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (ξ : U) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : ‖iteratedFDeriv ℝ n (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) (terminal δ hδ ξ)) a‖ ≤ scalarJetCost δ * ‖ξ‖ * terminalMass * EulerGevrey.majorant (jetRadius δ) 0 n

noncomputable def EulerPacketTerminalDatum.wordRadius (ι : Type u_1) [Fintype ι] (δ : ℝ) : ℝ

Word radius, given by sobolevCoefficientRadius ι (jetRadius δ).

Equations

• EulerPacketTerminalDatum.wordRadius ι δ = EulerParameterWordGevrey.sobolevCoefficientRadius ι (EulerPacketTerminalDatum.jetRadius δ)

noncomputable def EulerPacketTerminalDatum.wordCost (ι : Type u_1) [Fintype ι] (q : ℕ) (δ : ℝ) : ℝ

Word cost, given by sobolevCoefficientAmplitude ι q (jetRadius δ) (scalarJetCost δ * terminalMass).

Equations

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

theorem EulerPacketTerminalDatum.terminal_block_bound {ι : Type u_1} {U : Type u_2} [Fintype ι] [NormedAddCommGroup U] [NormedSpace ℝ U] (directions : ι → EulerLiftedGradientSpace.LiftTangent) (hd : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (ξ : U) (n : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) : EulerParameterWordGevrey.block directions q (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate period b) (terminal δ hδ ξ)) n a ≤ EulerParameterWordGevrey.sobolevCoefficientAmplitude ι q (jetRadius δ) (scalarJetCost δ * ‖ξ‖ * terminalMass) * EulerGevrey.majorant (wordRadius ι δ) 0 n