External derivative blocks with a fixed Sobolev index.

@[irreducible]

def EulerH6Pressure.SpatialJet.restrict {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (q : ℕ) (hq : q ≤ s) : EulerSpatialSobolevInverse.SpatialJet period directions q f

Retain any prescribed lower order of an actual strong derivative jet.

Equations

• One or more equations did not get rendered due to their size.
• EulerH6Pressure.SpatialJet.restrict J 0 x_1 = EulerSpatialSobolevInverse.SpatialJet.zero f
• EulerH6Pressure.SpatialJet.restrict (EulerSpatialSobolevInverse.SpatialJet.zero f) n.succ h = ⋯.elim

theorem EulerH6Pressure.SpatialJet.norm_unique {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (K : EulerSpatialSobolevInverse.SpatialJet period directions s g) (hfg : f = g) : J.sobolevNorm = K.sobolevNorm

@[irreducible]

def EulerH6Pressure.SpatialJet.wordJet {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {q n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions (q + n) f) (w : Fin n → Fin 4) : EulerSpatialSobolevInverse.SpatialJet period directions q (J.word w)

A derivative word carries the remaining genuine Sobolev jet.

Equations

• One or more equations did not get rendered due to their size.
• EulerH6Pressure.SpatialJet.wordJet J_2 w_2 = ⋯.mpr J_2

noncomputable def EulerH6Pressure.sobolevSize (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} (q : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : ℝ

The strong Sobolev norm of an L² field, set to zero off the Sobolev domain. Every use below supplies an actual derivative jet, so its value is the genuine jet norm.

Equations

• EulerH6Pressure.sobolevSize period q f = if h : Nonempty (EulerSpatialSobolevInverse.SpatialJet period directions q f) then (Classical.choice h).sobolevNorm else 0

theorem EulerH6Pressure.sobolevSize_eq (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {q : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions q f) : sobolevSize period q f = J.sobolevNorm

noncomputable def EulerH6Pressure.blockNorm (period : ℝ) [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (q n : ℕ) : ℝ

The external order-n block with a fixed base Sobolev index q.

Equations

• EulerH6Pressure.blockNorm period J q n = ∑ r ∈ Finset.range (q + 1), EulerJetProductBounds.levelNorm period J (n + r)

def EulerH6Pressure.coefficientBlock (period : ℝ) {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (q n : ℕ) : ℝ

Fixed-order coefficient multiplier blocks; the factor 2^q bounds the base Leibniz sums.

Equations

• EulerH6Pressure.coefficientBlock period K q n = 2 ^ q * ∑ r ∈ Finset.range (q + 1), EulerJetProductBounds.boundLevel period K (n + r)

@[irreducible]

def EulerH6Pressure.CoefficientJet.restrict {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (q : ℕ) (hq : q ≤ s) : EulerSpatialSobolevInverse.CoefficientJet period directions q A

Retain the prescribed base order of an actual coefficient derivative tree.

Equations

• One or more equations did not get rendered due to their size.
• EulerH6Pressure.CoefficientJet.restrict K 0 x_1 = EulerSpatialSobolevInverse.CoefficientJet.zero A
• EulerH6Pressure.CoefficientJet.restrict (EulerSpatialSobolevInverse.CoefficientJet.zero A) n.succ h = ⋯.elim

def EulerH6Pressure.SpatialJet.derivativeJet {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (w : Fin n → Fin 4) (h : n + q ≤ s) : EulerSpatialSobolevInverse.SpatialJet period directions q (J.word w)

The fixed-order strong jet of any valid external derivative word.

Equations

• EulerH6Pressure.SpatialJet.derivativeJet J w h = ⋯ ▸ EulerH6Pressure.SpatialJet.wordJet (EulerH6Pressure.SpatialJet.restrict J (q + n) ⋯) w

theorem EulerH6Pressure.sobolevSize_nonneg {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} (q : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : 0 ≤ sobolevSize period q f

theorem EulerH6Pressure.sobolevSize_add_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {q : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions q f) (K : EulerSpatialSobolevInverse.SpatialJet period directions q g) : sobolevSize period q (f + g) ≤ sobolevSize period q f + sobolevSize period q g

theorem EulerH6Pressure.sobolevSize_sub_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {q : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions q f) (K : EulerSpatialSobolevInverse.SpatialJet period directions q g) : sobolevSize period q (f - g) ≤ sobolevSize period q f + sobolevSize period q g

theorem EulerH6Pressure.blockNorm_nonneg {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) : 0 ≤ blockNorm period J q n

theorem EulerH6Pressure.coefficientBlock_nonneg {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) : 0 ≤ coefficientBlock period K q n

theorem EulerH6Pressure.blockNorm_truncate {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions (s + 1) f) (h : n + q ≤ s) : blockNorm period J.truncate q n = blockNorm period J q n

theorem EulerH6Pressure.coefficientBlock_truncate {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions (s + 1) A) (h : n + q ≤ s) : coefficientBlock period K.truncate q n = coefficientBlock period K q n

theorem EulerH6Pressure.blockNorm_succ {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions (s + 1) f) (q n : ℕ) : blockNorm period J q (n + 1) = match J with | EulerSpatialSobolevInverse.SpatialJet.succ derivatives lower hasDeriv => ∑ i : Fin 4, blockNorm period (lower i) q n

theorem EulerH6Pressure.coefficientBlock_succ {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (dA : Fin 4 → EulerSpatialSobolevInverse.SmoothCoefficient period) (lower : (i : Fin 4) → EulerSpatialSobolevInverse.CoefficientJet period directions s (dA i)) (hd : ∀ (i : Fin 4) (x : EulerLiftedGradientSpace.LiftDomain period), (dA i).coefficient x = EulerTransportDerivatives.fieldDerivative period (directions i) A.coefficient x) (q n : ℕ) : coefficientBlock period (EulerSpatialSobolevInverse.CoefficientJet.succ dA lower hd) q (n + 1) = ∑ i : Fin 4, coefficientBlock period (lower i) q n

theorem EulerH6Pressure.blockNorm_zero_eq_size {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (h : q ≤ s) : blockNorm period J q 0 = sobolevSize period q f

theorem EulerH6Pressure.blockNorm_eq_word_sizes {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (h : n + q ≤ s) : blockNorm period J q n = ∑ w : Fin n → Fin 4, sobolevSize period q (J.word w)

A fixed-index block is exactly the sum of the Sobolev norms of the external words.

theorem EulerH6Pressure.triangle_sum_le_product (q : ℕ) (A B : ℕ → ℝ) (hA : ∀ (n : ℕ), 0 ≤ A n) (hB : ∀ (n : ℕ), 0 ≤ B n) : ∑ r ∈ Finset.range (q + 1), ∑ l ∈ Finset.range (r + 1), A l * B (r - l) ≤ (∑ l ∈ Finset.range (q + 1), A l) * ∑ j ∈ Finset.range (q + 1), B j

The nonnegative lower-triangular convolution is bounded by the full product of sums.

theorem EulerH6Pressure.base_convolution_bound (q : ℕ) (A B : ℕ → ℝ) (hA : ∀ (n : ℕ), 0 ≤ A n) (hB : ∀ (n : ℕ), 0 ≤ B n) : ∑ r ∈ Finset.range (q + 1), EulerJetProductBounds.leibnizConvolution A B r ≤ (2 ^ q * ∑ l ∈ Finset.range (q + 1), A l) * ∑ j ∈ Finset.range (q + 1), B j

The fixed base-order Leibniz estimate has a constant independent of all external orders.

theorem EulerH6Pressure.blockNorm_add_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (K : EulerSpatialSobolevInverse.SpatialJet period directions s g) : blockNorm period (J.add K) q n ≤ blockNorm period J q n + blockNorm period K q n

theorem EulerH6Pressure.multiply_base_block_bound {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (h : q ≤ s) : blockNorm period (EulerSpatialSobolevInverse.SpatialJet.multiply K J) q 0 ≤ coefficientBlock period K q 0 * blockNorm period J q 0

Multiplication is bounded at the fixed base Sobolev order q.

theorem EulerH6Pressure.multiply_blockNorm_bound {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s q n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (h : n + q ≤ s) : blockNorm period (EulerSpatialSobolevInverse.SpatialJet.multiply K J) q n ≤ EulerJetProductBounds.leibnizConvolution (coefficientBlock period K q) (blockNorm period J q) n

Leibniz in external derivative order, with all fixed Sobolev derivatives inside the blocks.