Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.ConstantCoefficientDirichletBesov.StandardOverlapComparison

Coarse-graining support: #

Support.Deterministic.ConstantCoefficientDirichletBesov.StandardOverlapComparison

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

Standard/overlapping positive Besov comparison #

The key geometric observation is that every ordinary descendant cube appears as the overlapping cube of its middle child. This file starts the comparison API with the exact middle-child identities.

source
@[simp]
theorem HCPolySupport.overlapCubeScaleFactor_middleChildCube {d : ℕ} (Q : TriadicCube d) :
overlapCubeScaleFactor (middleChildCube Q) = cubeScaleFactor Q
source
@[simp]
theorem HCPolySupport.overlapCubeVolume_middleChildCube {d : ℕ} (Q : TriadicCube d) :
overlapCubeVolume (middleChildCube Q) = cubeVolume Q
source
@[simp]
theorem HCPolySupport.overlapCubeMeasure_middleChildCube {d : ℕ} (Q : TriadicCube d) :
overlapCubeMeasure (middleChildCube Q) = cubeMeasure Q
source
@[simp]
theorem HCPolySupport.normalizedOverlapCubeMeasure_middleChildCube {d : ℕ} (Q : TriadicCube d) :
normalizedOverlapCubeMeasure (middleChildCube Q) = normalizedCubeMeasure Q
source
@[simp]
theorem HCPolySupport.overlapCubeAverage_middleChildCube {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) :
overlapCubeAverage (middleChildCube Q) f = cubeAverage Q f
source
@[simp]
theorem HCPolySupport.overlapCubeAverageVec_middleChildCube {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) :
overlapCubeAverageVec (middleChildCube Q) u = cubeAverageVec Q u
source
@[simp]
theorem HCPolySupport.overlapCubeFluctuationVec_middleChildCube {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) :
overlapCubeFluctuationVec (middleChildCube Q) u = cubeFluctuationVec Q u
source
@[simp]
theorem HCPolySupport.overlapCubeLpNorm_middleChildCube {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] (Q : TriadicCube d) (p : ENNReal) (u : Vec d → E) :
overlapCubeLpNorm (middleChildCube Q) p u = cubeLpNorm Q p u
source
theorem HCPolySupport.overlapCubeLpNorm_middleChildCube_fluctuation {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) :
overlapCubeLpNorm (middleChildCube Q) 2 (overlapCubeFluctuationVec (middleChildCube Q) u) = cubeLpNorm Q 2 (cubeFluctuationVec Q u)
source
theorem HCPolySupport.overlapCentersAtDepth_card_le_three_pow_mul_descendantsAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
(overlapCentersAtDepth Q j).card ≤ 3 ^ d * (descendantsAtDepth Q j).card
source
theorem HCPolySupport.cubeBesovPositiveVectorDepthAverage_le_three_pow_mul_overlapping {d : ℕ} (Q : TriadicCube d) (u : Vec d → Vec d) (j : ℕ) :
cubeBesovPositiveVectorDepthAverage Q u j ≤ 3 ^ d * cubeBesovOverlappingPositiveVectorDepthAverage Q u j
source
theorem HCPolySupport.sq_cubeBesovPositiveVectorDepthSeminorm_le_three_pow_mul_overlapping {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (j : ℕ) :
cubeBesovPositiveVectorDepthSeminorm Q s u j ^ 2 ≤ 3 ^ d * cubeBesovOverlappingPositiveVectorDepthSeminorm Q s u j ^ 2
source
theorem HCPolySupport.sq_cubeBesovPositiveVectorPartialSeminormTwo_le_three_pow_mul_overlapping {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) :
cubeBesovPositiveVectorPartialSeminormTwo Q s N u ^ 2 ≤ 3 ^ d * cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u ^ 2
source
theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_le_sqrt_three_pow_mul_overlapping {d : ℕ} (Q : TriadicCube d) (s : ℝ) (N : ℕ) (u : Vec d → Vec d) :
cubeBesovPositiveVectorPartialSeminormTwo Q s N u ≤ √(3 ^ d) * cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u
source
theorem HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo_bddAbove_of_overlapping {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u)) :
BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo Q s N u)
source
theorem HCPolySupport.cubeBesovPositiveVectorSeminormTwo_le_sqrt_three_pow_mul_overlapping {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u)) :
cubeBesovPositiveVectorSeminormTwo Q s u ≤ √(3 ^ d) * cubeBesovOverlappingPositiveVectorSeminormTwo Q s u
source
theorem HCPolySupport.positiveVectorNormTwo_le_sqrt_three_pow_mul_overlappingNorm {d : ℕ} (Q : TriadicCube d) (s : ℝ) (u : Vec d → Vec d) (hBdd : BddAbove (Set.range fun (N : ℕ) => cubeBesovOverlappingPositiveVectorPartialSeminormTwo Q s N u)) :
√(vecNormSq (cubeAverageVec Q u)) + cubeBesovPositiveVectorSeminormTwo Q s u ≤ √(3 ^ d) * cubeBesovOverlappingPositiveVectorNormTwo Q s u