Coarse-graining support: Support.Multiscale.ProjectionConvergence

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

noncomputable def HCPolySupport.descendantContaining {d : ℕ} (Q : TriadicCube d) (x : Vec d) (n : ℕ) (hx : x ∈ cubeSet Q) : TriadicCube d

The unique depth-n descendant of Q whose half-open cube contains x.

Equations

• HCPolySupport.descendantContaining Q x n hx = Classical.choose ⋯

theorem HCPolySupport.descendantContaining_mem_descendantsAtDepth {d : ℕ} (Q : TriadicCube d) (x : Vec d) (n : ℕ) (hx : x ∈ cubeSet Q) : descendantContaining Q x n hx ∈ descendantsAtDepth Q n

theorem HCPolySupport.mem_cubeSet_descendantContaining {d : ℕ} (Q : TriadicCube d) (x : Vec d) (n : ℕ) (hx : x ∈ cubeSet Q) : x ∈ cubeSet (descendantContaining Q x n hx)

theorem HCPolySupport.cubeScaleFactor_descendantContaining {d : ℕ} (Q : TriadicCube d) (x : Vec d) (n : ℕ) (hx : x ∈ cubeSet Q) : cubeScaleFactor (descendantContaining Q x n hx) = cubeScaleFactor Q / 3 ^ n

theorem HCPolySupport.cubeRadius_descendantContaining {d : ℕ} (Q : TriadicCube d) (x : Vec d) (n : ℕ) (hx : x ∈ cubeSet Q) : cubeRadius (descendantContaining Q x n hx) = 1 / 2 * cubeScaleFactor Q * (1 / 3) ^ n

theorem HCPolySupport.ae_tendsto_cubeProjection_of_integrableOn {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (cubeSet Q) MeasureTheory.volume) : ∀ᵐ (x : Vec d) ∂MeasureTheory.volume.restrict (cubeSet Q), Filter.Tendsto (fun (n : ℕ) => cubeProjection Q n f x) Filter.atTop (nhds (f x))