Coarse-graining support:

Support.Sobolev.Foundations.CubeNeumannW22CZ.WeakInteriorDQ.CubeTranslationTransport

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

theorem HCPolySupport.cubeVolume_originCube_same_scale {d : ℕ} (Q : TriadicCube d) : cubeVolume (originCube d Q.scale) = cubeVolume Q

theorem HCPolySupport.cubeMeasure_originCube_map_addRight_eq {d : ℕ} (Q : TriadicCube d) : MeasureTheory.Measure.map (fun (x : Vec d) => x + triadicCubeShift Q) (cubeMeasure (originCube d Q.scale)) = cubeMeasure Q

theorem HCPolySupport.normalizedCubeMeasure_originCube_map_addRight_eq {d : ℕ} (Q : TriadicCube d) : MeasureTheory.Measure.map (fun (x : Vec d) => x + triadicCubeShift Q) (normalizedCubeMeasure (originCube d Q.scale)) = normalizedCubeMeasure Q

theorem HCPolySupport.measurePreserving_addRight_normalizedCubeMeasure_originCube {d : ℕ} (Q : TriadicCube d) : MeasureTheory.MeasurePreserving (fun (x : Vec d) => x + triadicCubeShift Q) (normalizedCubeMeasure (originCube d Q.scale)) (normalizedCubeMeasure Q)

theorem HCPolySupport.memLp_originCube_comp_addRight_of_memLp {d : ℕ} (Q : TriadicCube d) {p : ENNReal} {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F p (normalizedCubeMeasure Q)) : MeasureTheory.MemLp (fun (x : Vec d) => F (x + triadicCubeShift Q)) p (normalizedCubeMeasure (originCube d Q.scale))

theorem HCPolySupport.cubeLpNorm_originCube_comp_addRight_eq_of_memLp {d : ℕ} (Q : TriadicCube d) {F : Vec d → ℝ} (hF : MeasureTheory.MemLp F 2 (normalizedCubeMeasure Q)) : (cubeLpNorm (originCube d Q.scale) 2 fun (x : Vec d) => F (x + triadicCubeShift Q)) = cubeLpNorm Q 2 F

theorem HCPolySupport.cubeAverage_originCube_comp_addRight_eq {d : ℕ} (Q : TriadicCube d) (F : Vec d → ℝ) : (cubeAverage (originCube d Q.scale) fun (x : Vec d) => F (x + triadicCubeShift Q)) = cubeAverage Q F