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

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

theorem HCPolySupport.cubeLpNorm_infty_descendant_le {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (f : Vec d → Vec d) (hf : MeasureTheory.MemLp f ⊤ (normalizedCubeMeasure Q)) : cubeLpNorm R ⊤ f ≤ cubeLpNorm Q ⊤ f

theorem HCPolySupport.cubeLpNorm_add_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) (f g : Vec d → E) (hf : MeasureTheory.MemLp f p (normalizedCubeMeasure Q)) (hg : MeasureTheory.MemLp g p (normalizedCubeMeasure Q)) (hp : 1 ≤ p) : (cubeLpNorm Q p fun (x : Vec d) => f x + g x) ≤ cubeLpNorm Q p f + cubeLpNorm Q p g

theorem HCPolySupport.cubeLpNorm_two_cubeFluctuationVec_le_two_mul_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 (cubeFluctuationVec Q u) ≤ 2 * cubeLpNorm Q 2 u

theorem HCPolySupport.cubeLpNorm_two_cubeFluctuationVec_le_two_mul_cubeLpNorm_two_sub_const {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (c : Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 (cubeFluctuationVec Q u) ≤ 2 * cubeLpNorm Q 2 fun (x : Vec d) => u x - c

theorem HCPolySupport.cubeLpNorm_two_smul_le_mul_cubeLpNorm_infty {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (ξ : Vec d → Vec d) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) (hξ : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) : (cubeLpNorm Q 2 fun (x : Vec d) => v x • ξ x) ≤ cubeLpNorm Q ⊤ ξ * cubeLpNorm Q 2 v

theorem HCPolySupport.norm_cubeAverageVec_scalar_smul_le_cubeLpNorm_infty_mul_cubeLpNorm_two {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hξ : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) : ‖cubeAverageVec Q fun (x : Vec d) => u x • ξ x‖ ≤ cubeLpNorm Q ⊤ ξ * cubeLpNorm Q 2 u

theorem HCPolySupport.cubeLpNorm_two_scalarFluctuation_smul_const_le {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (c : Vec d) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) : (cubeLpNorm Q 2 fun (x : Vec d) => cubeFluctuation Q v x • c) ≤ ‖c‖ * cubeBesovOscillation Q 2 v

theorem HCPolySupport.cubeLpNorm_two_cubeFluctuationVec_scalar_smul_le_note_terms {d : ℕ} (Q : TriadicCube d) (v : Vec d → ℝ) (ξ : Vec d → Vec d) (hv : MeasureTheory.MemLp v 2 (normalizedCubeMeasure Q)) (hξ : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 (cubeFluctuationVec Q fun (x : Vec d) => v x • ξ x) ≤ 2 * ((cubeLpNorm Q ⊤ fun (x : Vec d) => ξ x - cubeAverageVec Q ξ) * cubeLpNorm Q 2 v + cubeLpNorm Q ⊤ ξ * cubeBesovOscillation Q 2 v)

theorem HCPolySupport.cubeLpNorm_two_cubeFluctuationVec_centered_scalar_smul_le_note_terms {d : ℕ} (Q : TriadicCube d) (u : Vec d → ℝ) (ξ : Vec d → Vec d) (hu : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)) (hξ : MeasureTheory.MemLp ξ ⊤ (normalizedCubeMeasure Q)) : cubeLpNorm Q 2 (cubeFluctuationVec Q fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 2 * (((cubeLpNorm Q ⊤ fun (x : Vec d) => ξ x - cubeAverageVec Q ξ) * cubeLpNorm Q 2 fun (x : Vec d) => u x - cubeAverage Q u) + cubeLpNorm Q ⊤ ξ * cubeBesovOscillation Q 2 fun (x : Vec d) => u x - cubeAverage Q u)

theorem HCPolySupport.cubeLpNorm_two_cubeFluctuationVec_scalar_smul_le_cutoff_terms_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) (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) : cubeLpNorm Q 2 (cubeFluctuationVec Q fun (x : Vec d) => v x • ξ x) ≤ 2 * (cubeScaleFactor Q * B * cubeLpNorm Q 2 v + cubeLpNorm Q ⊤ ξ * cubeBesovOscillation Q 2 v)

theorem HCPolySupport.cubeLpNorm_two_cubeFluctuationVec_centered_scalar_smul_le_cutoff_terms_of_contDiff_component_bound {d : ℕ} (Q : TriadicCube d) (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) : cubeLpNorm Q 2 (cubeFluctuationVec Q fun (x : Vec d) => (u x - cubeAverage Q u) • ξ x) ≤ 2 * ((cubeScaleFactor Q * B * cubeLpNorm Q 2 fun (x : Vec d) => u x - cubeAverage Q u) + cubeLpNorm Q ⊤ ξ * cubeBesovOscillation Q 2 fun (x : Vec d) => u x - cubeAverage Q u)