Coarse-graining support: Support.Multiscale.ProjectionLp

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

L^p wrappers for the projection layer.

This first checkpoint stays deliberately local: it packages the fact that cubeProjection is constant on each active descendant cube, then converts that pointwise statement into normalized cube L^p identities. It also records the constant-function behavior of cubeProjection and cubeIncrement.

theorem HCPolySupport.cubeProjection_ae_eq_cubeAverage_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (f : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) : cubeProjection Q j f =ᵐ[normalizedCubeMeasure R] fun (x : Vec d) => cubeAverage R f

theorem HCPolySupport.cubeProjection_ae_eq_cubeAverage_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (f : Vec d → ℝ) (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : cubeProjection Q (Q.scale - k).toNat f =ᵐ[normalizedCubeMeasure R] fun (x : Vec d) => cubeAverage R f

theorem HCPolySupport.cubeLpNorm_cubeProjection_eq_abs_cubeAverage_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (p : ENNReal) (f : Vec d → ℝ) (hR : R ∈ descendantsAtDepth Q j) (hp : p ≠ 0) : cubeLpNorm R p (cubeProjection Q j f) = ‖cubeAverage R f‖

theorem HCPolySupport.cubeLpNorm_cubeProjection_eq_abs_cubeAverage_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (p : ENNReal) (f : Vec d → ℝ) (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) (hp : p ≠ 0) : cubeLpNorm R p (cubeProjection Q (Q.scale - k).toNat f) = ‖cubeAverage R f‖

theorem HCPolySupport.cubeProjection_ae_eq_const {d : ℕ} (Q : TriadicCube d) (j : ℕ) (c : ℝ) : (cubeProjection Q j fun (x : Vec d) => c) =ᵐ[normalizedCubeMeasure Q] fun (x : Vec d) => c

theorem HCPolySupport.cubeLpNorm_cubeProjection_nonneg {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (j : ℕ) (f : Vec d → ℝ) : 0 ≤ cubeLpNorm Q p (cubeProjection Q j f)

theorem HCPolySupport.cubeLpNorm_cubeIncrement_nonneg {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (j : ℕ) (f : Vec d → ℝ) : 0 ≤ cubeLpNorm Q p (cubeIncrement Q j f)

theorem HCPolySupport.cubeLpNorm_cubeProjection_const {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (j : ℕ) (c : ℝ) (hp : p ≠ 0) : cubeLpNorm Q p (cubeProjection Q j fun (x : Vec d) => c) = ‖c‖

@[simp]

theorem HCPolySupport.cubeLpNorm_cubeProjection_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (j : ℕ) : cubeLpNorm Q p (cubeProjection Q j fun (x : Vec d) => 0) = 0

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

theorem HCPolySupport.cubeLpNorm_cubeIncrement_zero_const {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (c : ℝ) (hp : p ≠ 0) : cubeLpNorm Q p (cubeIncrement Q 0 fun (x : Vec d) => c) = ‖c‖

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

@[simp]

theorem HCPolySupport.cubeLpNorm_cubeIncrement_zero {d : ℕ} (Q : TriadicCube d) (p : ENNReal) (j : ℕ) : cubeLpNorm Q p (cubeIncrement Q j fun (x : Vec d) => 0) = 0