Documentation

LeanPool.HighContrastHomogenization.Support.Geometry.CubeMetric

Coarse-graining support: Support.Geometry.CubeMetric #

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

source
noncomputable def HCPolySupport.cubeCenter {d : ℕ} (Q : TriadicCube d) :
Vec d

The cube center with coordinates Q.index i times the cube scale factor.

Equations
Instances For
    source
    noncomputable def HCPolySupport.cubeRadius {d : ℕ} (Q : TriadicCube d) :
    ℝ

    Half the cube scale factor, the radius of the cube in the coordinate supremum norm.

    Equations
    Instances For
      source
      theorem HCPolySupport.cubeRadius_pos {d : ℕ} (Q : TriadicCube d) :
      0 < cubeRadius Q
      source
      theorem HCPolySupport.cubeRadius_nonneg {d : ℕ} (Q : TriadicCube d) :
      0 ≤ cubeRadius Q
      source
      theorem HCPolySupport.cubeScaleFactor_eq_two_mul_cubeRadius {d : ℕ} (Q : TriadicCube d) :
      cubeScaleFactor Q = 2 * cubeRadius Q
      source
      theorem HCPolySupport.cubeScaleFactor_eq_one_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (hQ : Q.scale = 0) :
      cubeScaleFactor Q = 1
      source
      theorem HCPolySupport.cubeRadius_eq_half_of_scale_eq_zero {d : ℕ} {Q : TriadicCube d} (hQ : Q.scale = 0) :
      cubeRadius Q = 1 / 2
      source
      theorem HCPolySupport.closedBall_cubeCenter_eq_pi_Icc {d : ℕ} (Q : TriadicCube d) :
      Metric.closedBall (cubeCenter Q) (cubeRadius Q) = Set.univ.pi fun (i : Fin d) => Set.Icc (cubeCenter Q i - cubeRadius Q) (cubeCenter Q i + cubeRadius Q)
      source
      theorem HCPolySupport.ball_cubeCenter_eq_openCubeSet {d : ℕ} (Q : TriadicCube d) :
      Metric.ball (cubeCenter Q) (cubeRadius Q) = openCubeSet Q
      source
      theorem HCPolySupport.cubeSet_subset_closedBall {d : ℕ} (Q : TriadicCube d) :
      cubeSet Q ⊆ Metric.closedBall (cubeCenter Q) (cubeRadius Q)
      source
      theorem HCPolySupport.cubeSet_ae_eq_closedBall {d : ℕ} (Q : TriadicCube d) :
      cubeSet Q =ᵐ[MeasureTheory.volume] Metric.closedBall (cubeCenter Q) (cubeRadius Q)
      source
      theorem HCPolySupport.cubeAverage_eq_setAverage_cubeSet {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) :
      cubeAverage Q f = ⨍ (x : Vec d) in cubeSet Q, f x
      source
      theorem HCPolySupport.cubeAverage_eq_setAverage_closedBall {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) :
      cubeAverage Q f = ⨍ (x : Vec d) in Metric.closedBall (cubeCenter Q) (cubeRadius Q), f x