Coarse-graining support: Support.Deterministic.WeakNormInterfaces.AECongruence

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

theorem HCPolySupport.cubeAverage_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f g : Vec d → ℝ} (hfg : f =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] g) : cubeAverage Q f = cubeAverage Q g

theorem HCPolySupport.cubeAverageVec_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {f g : Vec d → Vec d} (hfg : f =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] g) : cubeAverageVec Q f = cubeAverageVec Q g

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (huv : u =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] v) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q u j = cubeBesovNegativeVectorDepthAverage Q v j

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (huv : u =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] v) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q s u j = cubeBesovNegativeVectorDepthSeminorm Q s v j

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (N : ℕ) (huv : u =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] v) : cubeBesovNegativeVectorPartialSeminorm Q s N u = cubeBesovNegativeVectorPartialSeminorm Q s N v

theorem HCPolySupport.cubeBesovNegativeVectorSeminorm_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (huv : u =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] v) : cubeBesovNegativeVectorSeminorm Q s u = cubeBesovNegativeVectorSeminorm Q s v

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (N : ℕ) (huv : u =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] v) : cubeBesovNegativeVectorPartialSeminormTwo Q s N u = cubeBesovNegativeVectorPartialSeminormTwo Q s N v

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_eq_of_ae_eq_on_cubeSet {d : ℕ} {Q : TriadicCube d} {u v : Vec d → Vec d} (s : ℝ) (huv : u =ᵐ[MeasureTheory.volume.restrict (cubeSet Q)] v) : cubeBesovNegativeVectorSeminormTwo Q s u = cubeBesovNegativeVectorSeminormTwo Q s v

@[simp]

theorem HCPolySupport.cubeBesovNegativeVectorDepthAverage_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) : cubeBesovNegativeVectorDepthAverage Q 0 j = 0

@[simp]

theorem HCPolySupport.cubeBesovNegativeVectorDepthSeminorm_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (j : ℕ) : cubeBesovNegativeVectorDepthSeminorm Q s 0 j = 0

@[simp]

theorem HCPolySupport.cubeBesovNegativeVectorPartialSeminormTwo_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) : cubeBesovNegativeVectorPartialSeminormTwo Q s N 0 = 0

@[simp]

theorem HCPolySupport.cubeBesovNegativeVectorSeminormTwo_zero {d : ℕ} (Q : TriadicCube d) (s : ℝ) : cubeBesovNegativeVectorSeminormTwo Q s 0 = 0