Weighted Pressure

theorem EulerWeightedPressure.lower_triangle_sum_le_product (N : ℕ) (a b : ℕ → ℝ) (ha : ∀ (n : ℕ), 0 ≤ a n) (hb : ∀ (n : ℕ), 0 ≤ b n) : ∑ n ∈ Finset.range (N + 1), ∑ l ∈ Finset.range n, a (l + 1) * b (n - (l + 1)) ≤ (∑ l ∈ Finset.range (N + 1), a l) * ∑ j ∈ Finset.range (N + 1), b j

theorem EulerWeightedPressure.geometric_lower_triangle (q : ℝ) (hq : 0 ≤ q) (hhalf : q ≤ 1 / 2) (N : ℕ) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 ≤ b n) : ∑ n ∈ Finset.range (N + 1), ∑ l ∈ Finset.range n, q ^ (l + 1) * b (n - (l + 1)) ≤ 2 * q * ∑ j ∈ Finset.range (N + 1), b j

theorem EulerWeightedPressure.shifted_weight_kernel (ρ Rc : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (j l : ℕ) (Z : ℝ) (hZ : 0 ≤ Z) : ↑(j + l + 1) * EulerPacketWeights.weight ρ (j + l + 1) * ↑((j + l).choose l) * (Rc ^ l * ↑l.factorial ^ 2) * Z ≤ (ρ * Rc) ^ l * (↑(j + 1) * EulerPacketWeights.weight ρ (j + 1) * Z)

theorem EulerWeightedPressure.shifted_weighted_inverse (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (N : ℕ) (A F Z : ℕ → ℝ) (_hF : ∀ (n : ℕ), 0 ≤ F n) (hZ : ∀ (n : ℕ), 0 ≤ Z n) (hA : ∀ (l : ℕ), 1 ≤ l → l ≤ N → A l ≤ Rc ^ l * ↑l.factorial ^ 2) (hrec : ∀ n ≤ N, Z n ≤ M * (F n + ∑ l ∈ Finset.range n, ↑(n.choose (l + 1)) * A (l + 1) * Z (n - (l + 1)))) : ∑ n ∈ Finset.range (N + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * Z n ≤ 2 * M * ∑ n ∈ Finset.range (N + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * F n

A shifted Gevrey inverse estimate whose constant is independent of truncation. The positive-order coefficient terms are absorbed, rather than accumulated with order.

theorem EulerWeightedPressure.pressure_shifted_weighted_bound (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) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hcM : c⁻¹ ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ s → EulerJetProductBounds.boundLevel period K l ≤ EulerGevrey.majorant Rc 0 l) : ∑ n ∈ Finset.range (s + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * EulerJetProductBounds.levelNorm period (EulerSpatialSobolevInverse.SpatialJet.solvePressure K κ m c hc hpos J) n ≤ 2 * M * ∑ n ∈ Finset.range (s + 1), ↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * EulerJetProductBounds.levelNorm period J n

The shifted weighted operator bound for the pressure actually constructed in L².