Coarse-graining support: Support.Multiscale.Projection

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

@[simp]

theorem HCPolySupport.cubeIncrement_zero {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) : cubeIncrement Q 0 f = cubeProjection Q 0 f

@[simp]

theorem HCPolySupport.cubeIncrement_succ {d : ℕ} (Q : TriadicCube d) (n : ℕ) (f : Vec d → ℝ) : cubeIncrement Q (n + 1) f = fun (x : Vec d) => cubeProjection Q (n + 1) f x - cubeProjection Q n f x

theorem HCPolySupport.existsUnique_descendantAtDepth_mem_cubeSet {d : ℕ} {Q : TriadicCube d} {x : Vec d} (n : ℕ) (hx : x ∈ cubeSet Q) : ∃! R : TriadicCube d, R ∈ descendantsAtDepth Q n ∧ x ∈ cubeSet R

theorem HCPolySupport.existsUnique_descendantAtScale_mem_cubeSet {d : ℕ} {Q : TriadicCube d} {x : Vec d} {k : ℤ} (hk : k ≤ Q.scale) (hx : x ∈ cubeSet Q) : ∃! R : TriadicCube d, R ∈ descendantsAtScale Q k ∧ x ∈ cubeSet R

theorem HCPolySupport.cubeProjection_eq_zero_of_not_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) {x : Vec d} (hx : x ∉ cubeSet Q) : cubeProjection Q j f x = 0

theorem HCPolySupport.cubeProjection_eq_cubeAverage_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (f : Vec d → ℝ) {x : Vec d} (hR : R ∈ descendantsAtDepth Q j) (hxR : x ∈ cubeSet R) : cubeProjection Q j f x = cubeAverage R f

theorem HCPolySupport.cubeProjection_eq_cubeAverage_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (f : Vec d → ℝ) {x : Vec d} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) (hxR : x ∈ cubeSet R) : cubeProjection Q (Q.scale - k).toNat f x = cubeAverage R f

theorem HCPolySupport.cubeProjection_eq_cubeProjection_of_mem_same_descendant {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (f : Vec d → ℝ) {x y : Vec d} (hR : R ∈ descendantsAtDepth Q j) (hxR : x ∈ cubeSet R) (hyR : y ∈ cubeSet R) : cubeProjection Q j f x = cubeProjection Q j f y

theorem HCPolySupport.cubeProjection_eq_cubeProjection_of_mem_same_descendantAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (f : Vec d → ℝ) {x y : Vec d} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) (hxR : x ∈ cubeSet R) (hyR : y ∈ cubeSet R) : cubeProjection Q (Q.scale - k).toNat f x = cubeProjection Q (Q.scale - k).toNat f y

theorem HCPolySupport.cubeProjection_eq_zero_of_not_mem_descendantsAtDepth_union {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) {x : Vec d} (hx : x ∉ ⋃ R ∈ ↑(descendantsAtDepth Q j), cubeSet R) : cubeProjection Q j f x = 0

theorem HCPolySupport.cubeAverage_const {d : ℕ} (Q : TriadicCube d) (c : ℝ) : (cubeAverage Q fun (x : Vec d) => c) = c

theorem HCPolySupport.cubeProjection_const_of_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) {x : Vec d} (hx : x ∈ cubeSet Q) : cubeProjection Q j (fun (x : Vec d) => c) x = c

theorem HCPolySupport.cubeProjection_const_of_not_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) {x : Vec d} (hx : x ∉ cubeSet Q) : cubeProjection Q j (fun (x : Vec d) => c) x = 0

theorem HCPolySupport.cubeIncrement_eq_zero_of_not_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (j : ℕ) (f : Vec d → ℝ) {x : Vec d} (hx : x ∉ cubeSet Q) : cubeIncrement Q j f x = 0

theorem HCPolySupport.cubeIncrement_eq_sub_cubeProjection_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (f : Vec d → ℝ) {x : Vec d} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hxR : x ∈ cubeSet R) : cubeIncrement Q (j + 1) f x = cubeAverage R f - cubeProjection Q j f x

theorem HCPolySupport.cubeIncrement_eq_sub_cubeAverage_of_mem_descendantsAtDepth {d : ℕ} {Q R S : TriadicCube d} {j : ℕ} (f : Vec d → ℝ) {x : Vec d} (hR : R ∈ descendantsAtDepth Q (j + 1)) (hS : S ∈ descendantsAtDepth Q j) (hxR : x ∈ cubeSet R) (hxS : x ∈ cubeSet S) : cubeIncrement Q (j + 1) f x = cubeAverage R f - cubeAverage S f

theorem HCPolySupport.cubeIncrement_telescope {d : ℕ} (Q : TriadicCube d) (f : Vec d → ℝ) (x : Vec d) (n : ℕ) : ∑ j ∈ Finset.range (n + 1), cubeIncrement Q j f x = cubeProjection Q n f x

theorem HCPolySupport.cubeIncrement_zero_const_of_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (c : ℝ) {x : Vec d} (hx : x ∈ cubeSet Q) : cubeIncrement Q 0 (fun (x : Vec d) => c) x = c

theorem HCPolySupport.cubeIncrement_zero_const_of_not_mem_cubeSet {d : ℕ} (Q : TriadicCube d) (c : ℝ) {x : Vec d} (hx : x ∉ cubeSet Q) : cubeIncrement Q 0 (fun (x : Vec d) => c) x = 0

theorem HCPolySupport.cubeIncrement_succ_const {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) (x : Vec d) : cubeIncrement Q (j + 1) (fun (x : Vec d) => c) x = 0