Coarse-graining support: Support.Deterministic.CoarsePoincareRHS.SeminormRecurrence

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.cubeAverageVec_sub {d : ℕ} (Q : TriadicCube d) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) : (cubeAverageVec Q fun (x : Vec d) => u x - v x) = cubeAverageVec Q u - cubeAverageVec Q v

theorem HCPolySupport.cubeAverageVec_add {d : ℕ} (Q : TriadicCube d) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) : (cubeAverageVec Q fun (x : Vec d) => u x + v x) = cubeAverageVec Q u + cubeAverageVec Q v

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_eq_of_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (huv : ∀ x ∈ cubeSet Q, u x = v x) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q u j = cubeBesovNegativeVectorDepthAverage Q v j

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_eq_of_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (huv : ∀ x ∈ cubeSet Q, u x = v x) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q s u j = cubeBesovNegativeVectorDepthSeminorm Q s v j

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_eq_of_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (N : ℕ) (huv : ∀ x ∈ cubeSet Q, u x = v x) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u = cubeBesovNegativeVectorPartialSeminormTwo Q s N v

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_eq_of_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (huv : ∀ x ∈ cubeSet Q, u x = v x) : cubeBesovNegativeVectorSeminormTwo Q s u = cubeBesovNegativeVectorSeminormTwo Q s v

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_sub_le_two_mul_add {d : ℕ} (Q : TriadicCube d) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q (fun (x : Vec d) => u x - v x) j ≤ 2 * cubeBesovNegativeVectorDepthAverage Q u j + 2 * cubeBesovNegativeVectorDepthAverage Q v j

theorem HCPolySupport.sq_cubeBesovNegativeVectorDepthSeminorm_sub_le_two_mul_add {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q s (fun (x : Vec d) => u x - v x) j ^ 2 ≤ 2 * cubeBesovNegativeVectorDepthSeminorm Q s u j ^ 2 + 2 * cubeBesovNegativeVectorDepthSeminorm Q s v j ^ 2

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_sub_le_two_mul_add {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x - v x) ^ 2 ≤ 2 * cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 + 2 * cubeBesovNegativeVectorPartialSeminormTwo Q s N v ^ 2

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_add_le_two_mul_add {d : ℕ} (Q : TriadicCube d) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q (fun (x : Vec d) => u x + v x) j ≤ 2 * cubeBesovNegativeVectorDepthAverage Q u j + 2 * cubeBesovNegativeVectorDepthAverage Q v j

theorem HCPolySupport.sq_cubeBesovNegativeVectorDepthSeminorm_add_le_two_mul_add {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q s (fun (x : Vec d) => u x + v x) j ^ 2 ≤ 2 * cubeBesovNegativeVectorDepthSeminorm Q s u j ^ 2 + 2 * cubeBesovNegativeVectorDepthSeminorm Q s v j ^ 2

theorem HCPolySupport.sq_cubeBesovNegativeVectorPartialSeminormTwo_add_le_two_mul_add {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x + v x) ^ 2 ≤ 2 * cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 + 2 * cubeBesovNegativeVectorPartialSeminormTwo Q s N v ^ 2

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_add_le_sqrtTwo_mul_add {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x + v x) ≤ √2 * (cubeBesovNegativeVectorPartialSeminormTwo Q s N u + cubeBesovNegativeVectorPartialSeminormTwo Q s N v)

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_add_le_sqrtTwo_mul_add_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (hvBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N v)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => u x + v x) ≤ √2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s v)

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_sub_le_sqrtTwo_mul_add {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (N : ℕ) : (cubeBesovNegativeVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x - v x) ≤ √2 * (cubeBesovNegativeVectorPartialSeminormTwo Q s N u + cubeBesovNegativeVectorPartialSeminormTwo Q s N v)

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_sub_le_sqrtTwo_mul_add_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (hvBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N v)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => u x - v x) ≤ √2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s v)

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_add_sub_le_sqrtTwo_mul_add_sqrtTwo_mul_add_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u v w : Vec d → Vec d) (hu : MemVectorL2 (cubeSet Q) u) (hv : MemVectorL2 (cubeSet Q) v) (hw : MemVectorL2 (cubeSet Q) w) (huBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (hvBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N v)) (hwBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N w)) : (cubeBesovNegativeVectorSeminormTwo Q s fun (x : Vec d) => u x + v x - w x) ≤ √2 * (√2 * (cubeBesovNegativeVectorSeminormTwo Q s u + cubeBesovNegativeVectorSeminormTwo Q s v) + cubeBesovNegativeVectorSeminormTwo Q s w)

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_le_succ {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (N : ℕ) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_le_succ {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (N : ℕ) : cubeBesovPositiveVectorPartialSeminormTwo Q s N u ≤ cubeBesovPositiveVectorPartialSeminormTwo Q s (N + 1) u

theorem HCPolySupport.sq_cubeBesovNegativeVectorSeminormTwo_le_of_partialSqBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) {B : ℝ} (hB_nonneg : 0 ≤ B) (hpartial : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s N u ^ 2 ≤ B) : cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 ≤ B

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_le_seminormTwo_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) (N : ℕ) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u ≤ cubeBesovNegativeVectorSeminormTwo Q s u

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_le_seminormTwo_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u)) (N : ℕ) : cubeBesovPositiveVectorPartialSeminormTwo Q s N u ≤ cubeBesovPositiveVectorSeminormTwo Q s u

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N u)) : 0 ≤ cubeBesovNegativeVectorSeminormTwo Q s u

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_nonneg_of_bddAbove {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u)) : 0 ≤ cubeBesovPositiveVectorSeminormTwo Q s u

theorem HCPolySupport.sq_le_inv_one_sub_mul_add_of_sq_le_add_bilinear_term {A D U W G η : ℝ} (hη : 0 < η) (hη_lt : η < 1) (h : W ^ 2 ≤ A + D * (U + W) * G) : W ^ 2 ≤ (1 - η)⁻¹ * (A + η * U ^ 2 + 2 * η⁻¹ * (D / 2 * G) ^ 2)

theorem HCPolySupport.add_bilinear_term_le_add_eta_sq_add_invEta_sq {D U W G η : ℝ} (hη : 0 < η) : D * (U + W) * G ≤ η * U ^ 2 + η * W ^ 2 + 2 * η⁻¹ * (D / 2 * G) ^ 2

theorem HCPolySupport.sq_cubeBesovNegativeVectorSeminormTwo_le_descendantsAverage_add_of_succ_partialBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (Bchild : TriadicCube d → ℝ) {F : ℝ} (hB_nonneg : 0 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => Bchild R ^ 2) + F) (hlocal : ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo Q s (N + 1) u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => cubeBesovNegativeVectorPartialSeminormTwo R s N u ^ 2) + F) (hchild : ∀ R ∈ descendantsAtDepth Q 1, ∀ (N : ℕ), cubeBesovNegativeVectorPartialSeminormTwo R s N u ≤ Bchild R) : cubeBesovNegativeVectorSeminormTwo Q s u ^ 2 ≤ (Real.rpow 3 (-2 * s) * descendantsAverage Q 1 fun (R : TriadicCube d) => Bchild R ^ 2) + F

theorem HCPolySupport.real_forward_recurrence_iterate_le (R E : ℕ → ℝ) {γ : ℝ} (hγ : 0 ≤ γ) (hstep : ∀ (m : ℕ), R m ≤ γ * R (m + 1) + E m) (m N : ℕ) : R m ≤ γ ^ N * R (m + N) + ∑ k ∈ Finset.range N, γ ^ k * E (m + k)