Sharp order-by-order Leibniz bounds for actual cylinder Sobolev jets.

@[irreducible]

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

The sum of the L² norms of all actual derivative words of one order.

Equations

• EulerJetProductBounds.levelNorm period J 0 = ‖f‖
• EulerJetProductBounds.levelNorm period (EulerSpatialSobolevInverse.SpatialJet.zero f) n_2.succ = 0
• EulerJetProductBounds.levelNorm period (EulerSpatialSobolevInverse.SpatialJet.succ derivatives lower hasDeriv) n_2.succ = ∑ i : Fin 4, EulerJetProductBounds.levelNorm period (lower i) n_2

@[irreducible]

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

The sum of the uniform bounds of all coefficient derivatives of one order.

Equations

• One or more equations did not get rendered due to their size.
• EulerJetProductBounds.boundLevel period K 0 = ↑A.bound
• EulerJetProductBounds.boundLevel period (EulerSpatialSobolevInverse.CoefficientJet.zero A) n_2.succ = 0

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

theorem EulerJetProductBounds.boundLevel_nonneg {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) : 0 ≤ boundLevel period K n

theorem EulerJetProductBounds.levelNorm_eq_words {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) : levelNorm period J n = ∑ w : Fin n → Fin 4, ‖J.word w‖

The recursive level norm is exactly the finite sum over coordinate words.

theorem EulerJetProductBounds.levelNorm_truncate {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions (s + 1) f) (hn : n ≤ s) : levelNorm period J.truncate n = levelNorm period J n

theorem EulerJetProductBounds.boundLevel_truncate {period : ℝ} {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period directions (s + 1) A) (hn : n ≤ s) : boundLevel period K.truncate n = boundLevel period K n

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

def EulerJetProductBounds.leibnizConvolution (A B : ℕ → ℝ) (n : ℕ) : ℝ

Binomial convolution of nonnegative derivative-order bounds.

Equations

• EulerJetProductBounds.leibnizConvolution A B n = ∑ l ∈ Finset.range (n + 1), ↑(n.choose l) * A l * B (n - l)

theorem EulerJetProductBounds.leibnizConvolution_succ (A B : ℕ → ℝ) (n : ℕ) : leibnizConvolution A B (n + 1) = leibnizConvolution A (fun (k : ℕ) => B (k + 1)) n + leibnizConvolution (fun (k : ℕ) => A (k + 1)) B n

theorem EulerJetProductBounds.leibnizConvolution_congr (A B C D : ℕ → ℝ) (n : ℕ) (hA : ∀ l ≤ n, A l = C l) (hB : ∀ l ≤ n, B l = D l) : leibnizConvolution A B n = leibnizConvolution C D n

theorem EulerJetProductBounds.sum_leibnizConvolution_right (A : ℕ → ℝ) (B : Fin 4 → ℕ → ℝ) (n : ℕ) : ∑ i : Fin 4, leibnizConvolution A (B i) n = leibnizConvolution A (fun (l : ℕ) => ∑ i : Fin 4, B i l) n

theorem EulerJetProductBounds.sum_leibnizConvolution_left (A : Fin 4 → ℕ → ℝ) (B : ℕ → ℝ) (n : ℕ) : ∑ i : Fin 4, leibnizConvolution (A i) B n = leibnizConvolution (fun (l : ℕ) => ∑ i : Fin 4, A i l) B n

theorem EulerJetProductBounds.multiply_levelNorm_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (hn : n ≤ s) : levelNorm period (EulerSpatialSobolevInverse.SpatialJet.multiply K J) n ≤ leibnizConvolution (boundLevel period K) (levelNorm period J) n

Sharp binomial Leibniz estimate for the actual product jet, at every finite derivative order.

theorem EulerJetProductBounds.word_add {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {f g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (K : EulerSpatialSobolevInverse.SpatialJet period directions s g) (w : Fin n → Fin 4) : (J.add K).word w = J.word w + K.word w

def EulerJetProductBounds.commutatorConvolution (A B : ℕ → ℝ) (n : ℕ) : ℝ

Binomial derivative convolution with its undifferentiated-coefficient term removed.

Equations

• EulerJetProductBounds.commutatorConvolution A B n = EulerJetProductBounds.leibnizConvolution A B n - A 0 * B n

theorem EulerJetProductBounds.commutatorConvolution_eq_sum (A B : ℕ → ℝ) (n : ℕ) : commutatorConvolution A B n = ∑ l ∈ Finset.range n, ↑(n.choose (l + 1)) * A (l + 1) * B (n - (l + 1))

theorem EulerJetProductBounds.commutatorConvolution_congr (A B C D : ℕ → ℝ) (n : ℕ) (hA : ∀ l ≤ n, A l = C l) (hB : ∀ l ≤ n, B l = D l) : commutatorConvolution A B n = commutatorConvolution C D n

theorem EulerJetProductBounds.commutatorConvolution_succ (A B : ℕ → ℝ) (n : ℕ) : commutatorConvolution A B (n + 1) = commutatorConvolution A (fun (k : ℕ) => B (k + 1)) n + leibnizConvolution (fun (k : ℕ) => A (k + 1)) B n

theorem EulerJetProductBounds.sum_commutatorConvolution_right (A : ℕ → ℝ) (B : Fin 4 → ℕ → ℝ) (n : ℕ) : ∑ i : Fin 4, commutatorConvolution A (B i) n = commutatorConvolution A (fun (l : ℕ) => ∑ i : Fin 4, B i l) n

noncomputable def EulerJetProductBounds.commutatorLevel {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (n : ℕ) : ℝ

The actual product commutator at one derivative order, summed over coordinate words.

Equations

• EulerJetProductBounds.commutatorLevel K J n = ∑ w : Fin n → Fin 4, ‖(EulerSpatialSobolevInverse.SpatialJet.multiply K J).word w - A.operator (J.word w)‖

theorem EulerJetProductBounds.sum_word_snoc (n : ℕ) (F : (Fin (n + 1) → Fin 4) → ℝ) : ∑ w : Fin (n + 1) → Fin 4, F w = ∑ i : Fin 4, ∑ w : Fin n → Fin 4, F (Fin.snoc w i)

theorem EulerJetProductBounds.multiply_word_snoc {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (dA : Fin 4 → EulerSpatialSobolevInverse.SmoothCoefficient period) (lowerA : (i : Fin 4) → EulerSpatialSobolevInverse.CoefficientJet period directions s (dA i)) (hA : ∀ (i : Fin 4) (x : EulerLiftedGradientSpace.LiftDomain period), (dA i).coefficient x = EulerTransportDerivatives.fieldDerivative period (directions i) A.coefficient x) (df : Fin 4 → ↥(EulerLiftedGradientSpace.LiftL2 period)) (lowerF : (i : Fin 4) → EulerSpatialSobolevInverse.SpatialJet period directions s (df i)) (hF : ∀ (i : Fin 4), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (directions i) t)) f) (df i) 0) (i : Fin 4) (w : Fin n → Fin 4) : (EulerSpatialSobolevInverse.SpatialJet.multiply (EulerSpatialSobolevInverse.CoefficientJet.succ dA lowerA hA) (EulerSpatialSobolevInverse.SpatialJet.succ df lowerF hF)).word (Fin.snoc w i) = (EulerSpatialSobolevInverse.SpatialJet.multiply (EulerSpatialSobolevInverse.CoefficientJet.succ dA lowerA hA).truncate (lowerF i)).word w + (EulerSpatialSobolevInverse.SpatialJet.multiply (lowerA i) (EulerSpatialSobolevInverse.SpatialJet.succ df lowerF hF).truncate).word w

theorem EulerJetProductBounds.commutatorLevel_succ_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (dA : Fin 4 → EulerSpatialSobolevInverse.SmoothCoefficient period) (lowerA : (i : Fin 4) → EulerSpatialSobolevInverse.CoefficientJet period directions s (dA i)) (hA : ∀ (i : Fin 4) (x : EulerLiftedGradientSpace.LiftDomain period), (dA i).coefficient x = EulerTransportDerivatives.fieldDerivative period (directions i) A.coefficient x) (df : Fin 4 → ↥(EulerLiftedGradientSpace.LiftL2 period)) (lowerF : (i : Fin 4) → EulerSpatialSobolevInverse.SpatialJet period directions s (df i)) (hF : ∀ (i : Fin 4), HasDerivAt (fun (t : ℝ) => (EulerLiftedGradientSpace.translation period (EulerPressureSpatialRegularity.translationPath period (directions i) t)) f) (df i) 0) : commutatorLevel (EulerSpatialSobolevInverse.CoefficientJet.succ dA lowerA hA) (EulerSpatialSobolevInverse.SpatialJet.succ df lowerF hF) (n + 1) ≤ ∑ i : Fin 4, (commutatorLevel (EulerSpatialSobolevInverse.CoefficientJet.succ dA lowerA hA).truncate (lowerF i) n + levelNorm period (EulerSpatialSobolevInverse.SpatialJet.multiply (lowerA i) (EulerSpatialSobolevInverse.SpatialJet.succ df lowerF hF).truncate) n)

theorem EulerJetProductBounds.commutatorLevel_le {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (hn : n ≤ s) : commutatorLevel K J n ≤ commutatorConvolution (boundLevel period K) (levelNorm period J) n

Sharp all-order commutator estimate, with only positive coefficient derivative orders.

theorem EulerJetProductBounds.pressure_level_recurrence {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (K : EulerSpatialSobolevInverse.CoefficientJet period directions s A) (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (hn : n ≤ s) : levelNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) n ≤ c⁻¹ * (levelNorm period J n + ∑ l ∈ Finset.range n, ↑(n.choose (l + 1)) * boundLevel period K (l + 1) * levelNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) (n - (l + 1)))

The all-order pressure recurrence for actual L² derivative words, with the entire positive-order coefficient convolution derived from the product rule.

theorem EulerJetProductBounds.levelNorm_eq_zero_of_lt {period : ℝ} [Fact (0 < period)] {directions : Fin 4 → EulerLiftedGradientSpace.LiftTangent} {s n : ℕ} {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (J : EulerSpatialSobolevInverse.SpatialJet period directions s f) (hn : s < n) : levelNorm period J n = 0

A finite jet has no stored derivatives above its order.