Documentation

LeanPool.HighContrastHomogenization.Support.Geometry.OverlapCenters

Coarse-graining support: Support.Geometry.OverlapCenters #

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

source
noncomputable def HCPolySupport.ScalarOverlap.centersAtDepth {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
Finset (TriadicCube d)

Fine-grid centers used by the overlapping norm at depth j.

The centers are descendants one generation below the cube scale. We retain only those centers whose overlapping cube lies inside the parent cube.

Equations
Instances For
    source
    theorem HCPolySupport.ScalarOverlap.mem_centersAtDepth_iff {d : ℕ} {Q S : TriadicCube d} {j : ℕ} :
    S ∈ centersAtDepth Q j ↔ S ∈ descendantsAtDepth Q (j + 1) ∧ cubeSet S ⊆ HCPolySupport.cubeSet Q
    source
    theorem HCPolySupport.ScalarOverlap.mem_descendantsAtDepth_of_mem_centersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ centersAtDepth Q j) :
    S ∈ descendantsAtDepth Q (j + 1)
    source
    theorem HCPolySupport.ScalarOverlap.cubeSet_subset_cubeSet_of_mem_centersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ centersAtDepth Q j) :
    cubeSet S ⊆ HCPolySupport.cubeSet Q
    source
    theorem HCPolySupport.ScalarOverlap.openCubeSet_subset_openCubeSet_of_mem_centersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ centersAtDepth Q j) :
    openCubeSet S ⊆ HCPolySupport.openCubeSet Q
    source
    theorem HCPolySupport.ScalarOverlap.scaleFactor_eq_cubeScaleFactor_div_pow_of_mem_centersAtDepth {d : ℕ} {Q S : TriadicCube d} {j : ℕ} (hS : S ∈ centersAtDepth Q j) :
    scaleFactor S = cubeScaleFactor Q / 3 ^ j
    source
    theorem HCPolySupport.ScalarOverlap.eq_middleChildCube_of_mem_childCubes_of_cubeSet_subset {d : ℕ} {Q S : TriadicCube d} (hS : S ∈ childCubes Q) (hsub : cubeSet S ⊆ HCPolySupport.cubeSet Q) :
    S = middleChildCube Q
    source
    theorem HCPolySupport.ScalarOverlap.middleChildCube_mem_centersAtDepth_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :
    middleChildCube R ∈ centersAtDepth Q j
    source
    @[simp]
    theorem HCPolySupport.ScalarOverlap.centersAtDepth_zero {d : ℕ} (Q : TriadicCube d) :
    centersAtDepth Q 0 = {middleChildCube Q}
    source
    theorem HCPolySupport.ScalarOverlap.exists_mem_centersAtDepth_of_mem_cubeSet {d : ℕ} {Q : TriadicCube d} {x : Vec d} (j : ℕ) (hx : x ∈ HCPolySupport.cubeSet Q) :
    ∃ S ∈ centersAtDepth Q j, x ∈ cubeSet S
    source
    theorem HCPolySupport.ScalarOverlap.centersAtDepth_nonempty {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
    (centersAtDepth Q j).Nonempty
    source
    theorem HCPolySupport.ScalarOverlap.centersAtDepth_card_pos {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
    0 < (centersAtDepth Q j).card
    source
    theorem HCPolySupport.ScalarOverlap.centersAtDepth_card_ne_zero {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
    (centersAtDepth Q j).card ≠ 0
    source
    theorem HCPolySupport.ScalarOverlap.centersAtDepth_card_le_descendantsAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
    (centersAtDepth Q j).card ≤ (descendantsAtDepth Q (j + 1)).card
    source
    theorem HCPolySupport.ScalarOverlap.centersAtDepth_card_le_pow {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
    (centersAtDepth Q j).card ≤ (3 ^ d) ^ (j + 1)
    source
    theorem HCPolySupport.ScalarOverlap.descendantsAtDepth_card_le_centersAtDepth_card {d : ℕ} (Q : TriadicCube d) (j : ℕ) :
    (descendantsAtDepth Q j).card ≤ (centersAtDepth Q j).card
    source
    noncomputable def HCPolySupport.ScalarOverlap.centersAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) :
    ℝ

    Average over the overlapping centers at a fixed depth.

    Equations
    Instances For
      source
      theorem HCPolySupport.ScalarOverlap.centersAverage_le_centersAverage {d : ℕ} (Q : TriadicCube d) (j : ℕ) {F G : TriadicCube d → ℝ} (hFG : ∀ S ∈ centersAtDepth Q j, F S ≤ G S) :
      centersAverage Q j F ≤ centersAverage Q j G
      source
      theorem HCPolySupport.ScalarOverlap.centersAverage_const_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (hD : (centersAtDepth Q j).Nonempty) :
      (centersAverage Q j fun (x : TriadicCube d) => c) = c
      source
      theorem HCPolySupport.ScalarOverlap.centersAverage_const {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) :
      (centersAverage Q j fun (x : TriadicCube d) => c) = c
      source
      theorem HCPolySupport.ScalarOverlap.centersAverage_nonneg {d : ℕ} (Q : TriadicCube d) (j : ℕ) (F : TriadicCube d → ℝ) (hF : ∀ S ∈ centersAtDepth Q j, 0 ≤ F S) :
      0 ≤ centersAverage Q j F