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

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

theorem HCPolySupport.cubeScaleFactor_nonneg {d : ℕ} (Q : TriadicCube d) : 0 ≤ cubeScaleFactor Q

theorem HCPolySupport.cubeLpNorm_infty_le_of_bound_on_cubeSet {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (f : Vec d → E) {C : ℝ} (hC : 0 ≤ C) (hbound : ∀ x ∈ cubeSet Q, ‖f x‖ ≤ C) : cubeLpNorm Q ⊤ f ≤ C

theorem HCPolySupport.convex_cubeSet {d : ℕ} (Q : TriadicCube d) : Convex ℝ (cubeSet Q)

theorem HCPolySupport.norm_sub_le_cubeScaleFactor_of_mem_cubeSet {d : ℕ} (Q : TriadicCube d) {x y : Vec d} (hx : x ∈ cubeSet Q) (hy : y ∈ cubeSet Q) : ‖x - y‖ ≤ cubeScaleFactor Q

theorem HCPolySupport.norm_sub_le_cubeScaleFactor_mul_of_contDiff_bound {d : ℕ} (Q : TriadicCube d) {u : Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) {B : ℝ} (hB : 0 ≤ B) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) {x y : Vec d} (hx : x ∈ cubeSet Q) (hy : y ∈ cubeSet Q) : ‖u x - u y‖ ≤ cubeScaleFactor Q * B

theorem HCPolySupport.norm_sub_le_cubeScaleFactor_mul_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) {ξ : Vec d → Vec d} {B : ℝ} (hB : 0 ≤ B) (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) {x y : Vec d} (hx : x ∈ cubeSet Q) (hy : y ∈ cubeSet Q) : ‖ξ x - ξ y‖ ≤ cubeScaleFactor Q * B

theorem HCPolySupport.cubeLpNorm_component_le_cubeLpNorm {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (u : Vec d → Vec d) (i : Fin d) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) : (cubeLpNorm Q p fun (x : Vec d) => u x i) ≤ cubeLpNorm Q p u

theorem HCPolySupport.norm_cubeAverageVec_le_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : ‖cubeAverageVec Q u‖ ≤ cubeLpNorm Q 2 u

theorem HCPolySupport.norm_cubeAverageVec_le_cubeLpNorm_infty {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) : ‖cubeAverageVec Q u‖ ≤ cubeLpNorm Q ⊤ u

theorem HCPolySupport.cubeAverage_sub_const {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (c : ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeAverage Q fun (x : Vec d) => u x - c) = cubeAverage Q u - c

@[simp]

theorem HCPolySupport.cubeFluctuation_sub_const {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (c : ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : (cubeFluctuation Q fun (x : Vec d) => u x - c) = cubeFluctuation Q u

theorem HCPolySupport.norm_sub_cubeAverageVec_le_cubeLpNorm_infty_sub_const {d : ℕ} (Q : TriadicCube d) (ξ : Vec d → Vec d) (x : Vec d) (hξ : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) : ‖ξ x - cubeAverageVec Q ξ‖ ≤ cubeLpNorm Q ⊤ fun (y : Vec d) => ξ y - ξ x

theorem HCPolySupport.norm_sub_cubeAverageVec_le_cubeScaleFactor_mul_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) {ξ : Vec d → Vec d} {B : ℝ} (hB : 0 ≤ B) (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) {x : Vec d} (hx : x ∈ cubeSet Q) : ‖ξ x - cubeAverageVec Q ξ‖ ≤ cubeScaleFactor Q * B

theorem HCPolySupport.cubeLpNorm_infty_sub_cubeAverageVec_le_cubeScaleFactor_mul_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) {ξ : Vec d → Vec d} {B : ℝ} (hB : 0 ≤ B) (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) : (cubeLpNorm Q ⊤ fun (x : Vec d) => ξ x - cubeAverageVec Q ξ) ≤ cubeScaleFactor Q * B

theorem HCPolySupport.norm_cubeAverage_le_cubeLpNorm_infty {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (hu : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) : ‖cubeAverage Q u‖ ≤ cubeLpNorm Q ⊤ u

theorem HCPolySupport.norm_cubeAverage_le_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : ‖cubeAverage Q u‖ ≤ cubeLpNorm Q 2 u

theorem HCPolySupport.norm_sub_cubeAverage_le_cubeLpNorm_infty_sub_const {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (x : Vec d) (hu : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) : ‖u x - cubeAverage Q u‖ ≤ cubeLpNorm Q ⊤ fun (y : Vec d) => u y - u x

theorem HCPolySupport.cubeLpNorm_infty_sub_cubeAverage_le_cubeScaleFactor_mul_of_contDiff_bound {d : ℕ} (Q : TriadicCube d) {u : Vec d → ℝ} {B : ℝ} (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : (cubeLpNorm Q ⊤ fun (x : Vec d) => u x - cubeAverage Q u) ≤ cubeScaleFactor Q * B

theorem HCPolySupport.cubeLpNorm_two_le_cubeLpNorm_infty_of_memLp_infty {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (hu : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 u ≤ cubeLpNorm Q ⊤ u

theorem HCPolySupport.cubeBesovOscillation_two_le_cubeScaleFactor_mul_of_contDiff_bound {d : ℕ} (Q : TriadicCube d) {u : Vec d → ℝ} {B : ℝ} (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovOscillation Q 2 u ≤ cubeScaleFactor Q * B

theorem HCPolySupport.cubeBesovDepthSeminorm_one_two_le_of_contDiff_bound {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (j : ℕ) {B : ℝ} (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovDepthSeminorm Q 1 2 u j ≤ B

theorem HCPolySupport.cubeBesovPartialSeminormTop_one_two_le_of_contDiff_bound {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) {B : ℝ} (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovPartialSeminormTop Q 1 2 N u ≤ B

theorem HCPolySupport.cubeBesovPartialNormTop_one_two_le_of_contDiff_bound {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) {B : ℝ} (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovPartialNormTop Q 1 2 N u ≤ B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ u

theorem HCPolySupport.cubeBesovDualTestNorm_one_two_le_of_contDiff_bound {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) {B : ℝ} (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovDualTestNorm Q 1 2 1 N u ≤ B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ u

theorem HCPolySupport.cubeBesovDepthSeminorm_two_le_scaleWeight_mul_scaleFactor_mul_of_contDiff_bound_of_le_one {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (j : ℕ) {s B : ℝ} (hs1 : s ≤ 1) (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovDepthSeminorm Q s 2 u j ≤ cubeBesovScaleWeight s Q * cubeScaleFactor Q * B

theorem HCPolySupport.cubeBesovPartialSeminormTop_two_le_scaleBound_of_contDiff {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) {s B : ℝ} (hs1 : s ≤ 1) (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovPartialSeminormTop Q s 2 N u ≤ cubeBesovScaleWeight s Q * cubeScaleFactor Q * B

theorem HCPolySupport.cubeBesovPartialNormTop_two_le_scaleWeight_mul_of_contDiff_bound_of_le_one {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) {s B : ℝ} (hs1 : s ≤ 1) (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovPartialNormTop Q s 2 N u ≤ cubeBesovScaleWeight s Q * (cubeScaleFactor Q * B + cubeLpNorm Q ⊤ u)

theorem HCPolySupport.cubeBesovDualTestNorm_two_one_le_scaleWeight_mul_of_contDiff_bound_of_le_one {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (N : ℕ) {s B : ℝ} (hs1 : s ≤ 1) (hB : 0 ≤ B) (huLp : MeasureTheory.MemLp u ⊤ (normalizedCubeMeasure Q)) (hu : ContDiff ℝ (↑⊤) u) (hderiv : ∀ z ∈ cubeSet Q, ‖fderiv ℝ u z‖ ≤ B) : cubeBesovDualTestNorm Q s 2 1 N u ≤ cubeBesovScaleWeight s Q * (cubeScaleFactor Q * B + cubeLpNorm Q ⊤ u)

theorem HCPolySupport.cubeBesovDualTestNorm_one_two_component_le_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) (ξ : Vec d → Vec d) (i : Fin d) (N : ℕ) {B : ℝ} (hB : 0 ≤ B) (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) : (cubeBesovDualTestNorm Q 1 2 1 N fun (x : Vec d) => ξ x i) ≤ B + cubeBesovScaleWeight 1 Q * cubeLpNorm Q ⊤ ξ