Coarse-graining support: Support.Multiscale.OverlapLp

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

noncomputable def HCPolySupport.ScalarOverlap.cubeAverage {d : ℕ} (S : TriadicCube d) (f : Vec d → ℝ) : ℝ

Average of a scalar field on an overlapping cube.

Equations

• HCPolySupport.ScalarOverlap.cubeAverage S f = (HCPolySupport.ScalarOverlap.cubeVolume S)⁻¹ * ∫ (x : HCPolySupport.Vec d) in HCPolySupport.ScalarOverlap.cubeSet S, f x

noncomputable def HCPolySupport.ScalarOverlap.cubeAverageVec {d : ℕ} (S : TriadicCube d) (u : Vec d → Vec d) : Vec d

Coordinatewise average of a vector field on an overlapping cube.

Equations

• HCPolySupport.ScalarOverlap.cubeAverageVec S u i = HCPolySupport.ScalarOverlap.cubeAverage S fun (x : HCPolySupport.Vec d) => u x i

noncomputable def HCPolySupport.ScalarOverlap.cubeLpNorm {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (u : Vec d → E) : ℝ

Normalized L^p norm on an overlapping cube.

Equations

• HCPolySupport.ScalarOverlap.cubeLpNorm S p u = (MeasureTheory.eLpNorm u p (HCPolySupport.ScalarOverlap.normalizedCubeMeasure S)).toReal

theorem HCPolySupport.ScalarOverlap.cubeAverage_eq_integral_normalizedCubeMeasure {d : ℕ} (S : TriadicCube d) (f : Vec d → ℝ) : cubeAverage S f = ∫ (x : Vec d), f x ∂normalizedCubeMeasure S

@[simp]

theorem HCPolySupport.ScalarOverlap.cubeMeasure_middleChildCube {d : ℕ} (Q : TriadicCube d) : cubeMeasure (middleChildCube Q) = HCPolySupport.cubeMeasure Q

@[simp]

theorem HCPolySupport.ScalarOverlap.normalizedCubeMeasure_middleChildCube {d : ℕ} (Q : TriadicCube d) : normalizedCubeMeasure (middleChildCube Q) = HCPolySupport.normalizedCubeMeasure Q

@[simp]

theorem HCPolySupport.ScalarOverlap.cubeAverage_middleChildCube {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : cubeAverage (middleChildCube Q) f = HCPolySupport.cubeAverage Q f

theorem HCPolySupport.ScalarOverlap.cubeAverage_congr_on_cubeSet {d : ℕ} {S : TriadicCube d} {u v : Vec d → ℝ} (h : ∀ x ∈ cubeSet S, u x = v x) : cubeAverage S u = cubeAverage S v

theorem HCPolySupport.ScalarOverlap.cubeLpNorm_congr_on_cubeSet_generic {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) {u v : Vec d → E} (h : ∀ x ∈ cubeSet S, u x = v x) : cubeLpNorm S p u = cubeLpNorm S p v

@[simp]

theorem HCPolySupport.ScalarOverlap.cubeAverage_const {d : ℕ} (S : TriadicCube d) (c : ℝ) : (cubeAverage S fun (x : Vec d) => c) = c

@[simp]

theorem HCPolySupport.ScalarOverlap.cubeAverageVec_const {d : ℕ} (S : TriadicCube d) (c : Vec d) : (cubeAverageVec S fun (x : Vec d) => c) = c

theorem HCPolySupport.ScalarOverlap.cubeLpNorm_nonneg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (f : Vec d → E) : 0 ≤ cubeLpNorm S p f

@[simp]

theorem HCPolySupport.ScalarOverlap.cubeLpNorm_middleChildCube {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) (u : Vec d → E) : cubeLpNorm (middleChildCube Q) p u = HCPolySupport.cubeLpNorm Q p u

theorem HCPolySupport.ScalarOverlap.cubeLpNorm_const {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (c : E) (hp : p ≠ 0) : (cubeLpNorm S p fun (x : Vec d) => c) = ‖c‖

theorem HCPolySupport.ScalarOverlap.cubeLpNorm_zero {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (S : TriadicCube d) (p : ENNReal) (hp : p ≠ 0) : (cubeLpNorm S p fun (x : Vec d) => 0) = 0