Cutoff-independent comparison between actual Sobolev Gevrey sums and the source's metric root energies.

Exact identification of the source's base-Sobolev word sum and root metric energy.

@[reducible, inline]

abbrev EulerBaseWordMetric.BaseWord (s : ℕ) : Type

A base Sobolev word of any length at most s.

Equations

• EulerBaseWordMetric.BaseWord s = ((n : Fin (s + 1)) × (Fin ↑n → Fin 4))

noncomputable def EulerBaseWordMetric.baseWordValues (period : ℝ) [Fact (0 < period)] {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) : BaseWord s → ↥(EulerLiftedGradientSpace.LiftL2 period)

The finite family of actual strong derivatives indexed by all base Sobolev words.

Equations

• EulerBaseWordMetric.baseWordValues period J w = J.word w.snd

theorem EulerBaseWordMetric.sum_baseWordValues_norm (period : ℝ) [Fact (0 < period)] {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) : ∑ w : BaseWord s, ‖baseWordValues period J w‖ = J.sobolevNorm

The sigma-indexed family gives exactly the previously proved strong Sobolev sum norm.

theorem EulerBaseWordMetric.card_baseWord (s : ℕ) : Fintype.card (BaseWord s) = ∑ n ∈ Finset.range (s + 1), 4 ^ n

The number of base derivative words depends only on the fixed Sobolev index.

noncomputable def EulerBaseWordMetric.baseWordMetricNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) : ℝ

The source's root-of-sum metric energy for all base Sobolev words.

Equations

• EulerBaseWordMetric.baseWordMetricNorm period K J = EulerFiniteMetricEnergy.familyMetricNorm K (EulerBaseWordMetric.baseWordValues period J)

theorem EulerBaseWordMetric.sobolevNorm_le_baseWordMetric (period : ℝ) [Fact (0 < period)] {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) (c : ℝ) (hc : 0 < c) (hK : ∀ (u : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖u‖ ^ 2 ≤ inner ℝ (K u) u) : J.sobolevNorm ≤ √↑(Fintype.card (BaseWord s)) / c * baseWordMetricNorm period K J

The Sobolev sum is controlled by its metric root with a fixed base-word cardinality constant.

theorem EulerBaseWordMetric.baseWordMetric_le_sobolevNorm (period : ℝ) [Fact (0 < period)] {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection s f) : baseWordMetricNorm period K J ≤ √‖K‖ * J.sobolevNorm

The metric root is controlled by the actual base Sobolev sum with no extra word-count factor.

@[reducible, inline]

abbrev EulerGevreyMetricComparison.ExternalWord (N : ℕ) : Type

All external derivative words through the selected cutoff.

Equations

• EulerGevreyMetricComparison.ExternalWord N = ((n : Fin (N + 1)) × (Fin ↑n → Fin 4))

noncomputable def EulerGevreyMetricComparison.energyValues (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ExternalWord N → EulerBaseWordMetric.BaseWord q → ↥(EulerLiftedGradientSpace.LiftL2 period)

Literal base derivatives of each external word of an actual Sobolev field.

Equations

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

theorem EulerGevreyMetricComparison.blockNorm_baseWords (period : ℝ) [Fact (0 < period)] {s q n : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (h : n + q ≤ s) : EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) q n = ∑ w : Fin n → Fin 4, (EulerH6Pressure.SpatialJet.derivativeJet (EulerCylinderSobolevSpace.toJet period u) w h).sobolevNorm

Exact rewriting of a valid external Sobolev block as the actual base-word derivative sums.

theorem EulerGevreyMetricComparison.blockNorm_metric_lower (period : ℝ) [Fact (0 < period)] {s q n : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (h : n + q ≤ s) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (c : ℝ) (hc : 0 < c) (hK : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (K v) v) : EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) q n ≤ √↑(Fintype.card (EulerBaseWordMetric.BaseWord q)) / c * ∑ w : Fin n → Fin 4, EulerBaseWordMetric.baseWordMetricNorm period K (EulerH6Pressure.SpatialJet.derivativeJet (EulerCylinderSobolevSpace.toJet period u) w h)

The lower comparison at one external order uses only the fixed number of base Sobolev words.

theorem EulerGevreyMetricComparison.blockNorm_metric_upper (period : ℝ) [Fact (0 < period)] {s q n : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (h : n + q ≤ s) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) : ∑ w : Fin n → Fin 4, EulerBaseWordMetric.baseWordMetricNorm period K (EulerH6Pressure.SpatialJet.derivativeJet (EulerCylinderSobolevSpace.toJet period u) w h) ≤ √‖K‖ * EulerH6Pressure.blockNorm period (EulerCylinderSobolevSpace.toJet period u) q n

The upper metric comparison is independent of the external word count.

theorem EulerGevreyMetricComparison.metricSum_eq (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedMetricSum ρ (fun (I : ExternalWord N) => ↑I.fst) K (energyValues period q N hN u) = ∑ n : Fin (N + 1), EulerPacketWeights.weight ρ ↑n * ∑ w : Fin ↑n → Fin 4, EulerBaseWordMetric.baseWordMetricNorm period K (EulerH6Pressure.SpatialJet.derivativeJet (EulerCylinderSobolevSpace.toJet period u) w ⋯)

The metric-weighted energy is exactly the external-word sum of fixed-base metric roots.

theorem EulerGevreyMetricComparison.weightedNorm_metric_lower (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (c : ℝ) (hc : 0 < c) (hK : ∀ (v : ↥(EulerLiftedGradientSpace.LiftL2 period)), c ^ 2 * ‖v‖ ^ 2 ≤ inner ℝ (K v) v) : EulerSobolevGevreyOperators.weightedNorm period q N ρ u ≤ √↑(Fintype.card (EulerBaseWordMetric.BaseWord q)) / c * EulerWeightedCylinderEnergy.weightedMetricSum ρ (fun (I : ExternalWord N) => ↑I.fst) K (energyValues period q N hN u)

The actual weighted Sobolev sum is controlled by metric roots with no external-cutoff constant.

theorem EulerGevreyMetricComparison.weightedNorm_metric_upper (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (K : ↥(EulerLiftedGradientSpace.LiftL2 period) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedMetricSum ρ (fun (I : ExternalWord N) => ↑I.fst) K (energyValues period q N hN u) ≤ √‖K‖ * EulerSobolevGevreyOperators.weightedNorm period q N ρ u

The actual metric weighted energy is bounded by its Sobolev counterpart without a cutoff factor.

theorem EulerGevreyMetricComparison.card_baseWord_six : Fintype.card (EulerBaseWordMetric.BaseWord 6) = 5461

At the fixed base index six the comparison uses exactly 5461 base words.