Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.CutoffProduct.VectorProduct

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

theorem HCPolySupport.cubeL2Scalar_scale_depth_term_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : Vec d → ℝ) (j : ℕ) : Real.rpow 3 (s * ↑j) * (descendantsAverage Q j fun (R : TriadicCube d) => (cubeScaleFactor R * cubeLpNorm R 2 v) ^ 2) ^ (1 / 2) = cubeScaleFactor Q * cubeL2ScalarDepthSeminorm Q (s - 1) v j

theorem HCPolySupport.cubeBesovPositiveVectorDepthSeminorm_scalar_smul_le_cutoff_terms_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) (v : Vec d → ℝ) (ξ : Vec d → Vec d) {B : ℝ} (hB : 0 ≤ B) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) : cubeBesovPositiveVectorDepthSeminorm Q s (fun (x : Vec d) => v x • ξ x) j ≤ 2 * (cubeScaleFactor Q * B * cubeL2ScalarDepthSeminorm Q (s - 1) v j + cubeLpNorm Q ⊤ ξ * cubeBesovPositiveScalarDepthSeminorm Q s v j)

theorem HCPolySupport.cubeBesovPositiveVectorPartial_smul_le_cutoff_of_componentBound {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (v : Vec d → ℝ) (ξ : Vec d → Vec d) {B : ℝ} (hB : 0 ≤ B) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => v x • ξ x) ≤ 2 * (cubeScaleFactor Q * B * cubeL2ScalarPartialSeminormTwo Q (s - 1) N v + cubeLpNorm Q ⊤ ξ * cubeBesovPositiveScalarPartialSeminormTwo Q s N v)

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_centered_scalar_smul_le_cutoff_terms {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → ℝ) (ξ : Vec d → Vec d) {B : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 2 * ((cubeScaleFactor Q * B * cubeL2ScalarPartialSeminormTwo Q (s - 1) N fun (x : Vec d) => u x - cubeAverage Q u) + cubeLpNorm Q ⊤ ξ * cubeBesovPositiveScalarPartialSeminormTwo Q s N fun (x : Vec d) => u x - cubeAverage Q u)

theorem HCPolySupport.cubeLpNorm_two_le_cubeBesovPartialNormTop_zero {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 v ≤ cubeBesovPartialNormTop Q 0 2 0 v

theorem HCPolySupport.CubeDescendantProjectedDualMeanZeroPoincareEstimate.restrict_to_descendant {d : ℕ} {Q R : TriadicCube d} {C : ℝ} {u g : Vec d → ℝ} {M j : ℕ} (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C u g M) (hR : R ∈ descendantsAtDepth Q j) (hj : j ≤ M) : CubeDescendantProjectedDualMeanZeroPoincareEstimate R C u g (M - j)

theorem HCPolySupport.cubeL2ScalarDepthAverage_eq_cubeLpNorm_two_sq {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (j : ℕ) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) : cubeL2ScalarDepthAverage Q v j = cubeLpNorm Q 2 v ^ 2

theorem HCPolySupport.cubeL2ScalarDepthSeminorm_eq_rpow_mul_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) (s : ℝ) (v : Vec d → ℝ) (j : ℕ) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) : cubeL2ScalarDepthSeminorm Q s v j = Real.rpow 3 (s * ↑j) * cubeLpNorm Q 2 v

theorem HCPolySupport.cubeBesovPartialNormTop_zero_le {d : ℕ} (Q : TriadicCube d) (s : ℝ) (p : ENNReal) (N : ℕ) (v : Vec d → ℝ) : cubeBesovPartialNormTop Q s p 0 v ≤ cubeBesovPartialNormTop Q s p N v

theorem HCPolySupport.rpow_three_weight_sq_eq_geometric_ratio_pow (s : ℝ) (j : ℕ) : Real.rpow 3 (s * ↑j) ^ 2 = Real.rpow 3 (2 * s) ^ j

theorem HCPolySupport.cubeL2ScalarPartialSeminormTwo_le_geometric_mul_cubeLpNorm_two_of_neg {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (v : Vec d → ℝ) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) (hs : s < 0) : cubeL2ScalarPartialSeminormTwo Q s N v ≤ √(1 - Real.rpow 3 (2 * s))⁻¹ * cubeLpNorm Q 2 v

theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_scalar_smul_le_note_poincare_cutoff_terms {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {B C : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) (hs0 : 0 < s) (hs1 : s < 1) (hC : 0 ≤ C) : (cubeBesovPositiveVectorPartialSeminormTwo Q s N fun (x : Vec d) => u x • ξ x) ≤ 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * cubeLpNorm Q 2 u) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * cubeBesovCircPartialNorm Q (1 - s) 2 1 N g)))

theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_scalar_smul_le_note_poincare_cutoff_terms {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u g : Vec d → ℝ) (ξ : Vec d → Vec d) {B C BcircS : ℝ} (hB : 0 ≤ B) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hproj : ∀ (N : ℕ), CubeDescendantProjectedDualMeanZeroPoincareEstimate Q C (cubeFluctuation Q u) g N) (hg : MeasureTheory.MemLp g 2 (normalizedCubeMeasure Q)) (hξLp : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) (hξ : ∀ (i : Fin d), ContDiff ℝ ↑⊤ fun (x : Vec d) => ξ x i) (hderiv : ∀ (i : Fin d), ∀ z ∈ cubeSet Q, ‖fderiv ℝ (fun (x : Vec d) => ξ x i) z‖ ≤ B) (hs0 : 0 < s) (hs1 : s < 1) (hC : 0 ≤ C) (hnegS : ∀ (N : ℕ), cubeBesovCircPartialNorm Q (1 - s) 2 1 N g ≤ BcircS) : (cubeBesovPositiveVectorSeminormTwo Q s fun (x : Vec d) => u x • ξ x) ≤ 2 * (cubeScaleFactor Q * B * (√(1 - Real.rpow 3 (2 * (s - 1)))⁻¹ * cubeLpNorm Q 2 u) + cubeLpNorm Q ⊤ ξ * (cubeBesovScaleWeight (-s) Q * (3 / 2 * C * 3 ^ (↑d + 1) * (1 - 3 ^ (-s))⁻¹ * BcircS)))