Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Foundation.Geometry

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

theorem HCPolySupport.isFiniteMeasureVolumeMeasureOnCubeSet {d : ℕ} (Q : TriadicCube d) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))

instance HCPolySupport.instIsFiniteMeasureVolumeMeasureOnCubeSet {d : ℕ} (Q : TriadicCube d) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))

noncomputable def HCPolySupport.fullBlockMatRowAbsSqBound {d : ℕ} (M : FullBlockMat d) : ℝ

The sum of squared absolute row sums of a full block matrix.

Equations

• HCPolySupport.fullBlockMatRowAbsSqBound M = ∑ i : HCPolySupport.BlockCoord d, (∑ j : HCPolySupport.BlockCoord d, |M i j|) ^ 2

theorem HCPolySupport.abs_fullBlockVec_le_one_of_fullBlockVecNormSq_eq_one {d : ℕ} {e : FullBlockVec d} (he : fullBlockVecNormSq e = 1) (i : BlockCoord d) : |e i| ≤ 1

theorem HCPolySupport.fullBlockVecNormSq_mulVec_le_rowAbsSqBound_of_eq_one {d : ℕ} (M : FullBlockMat d) {e : FullBlockVec d} (he : fullBlockVecNormSq e = 1) : fullBlockVecNormSq (Matrix.mulVec M e) ≤ fullBlockMatRowAbsSqBound M

theorem HCPolySupport.blockVecDot_ofFullBlockVec_self_eq_fullBlockVecNormSq {d : ℕ} (x : FullBlockVec d) : blockVecDot (ofFullBlockVec x) (ofFullBlockVec x) = fullBlockVecNormSq x

theorem HCPolySupport.descendant_scale_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) : k ≤ Q.scale

theorem HCPolySupport.descendant_scale_eq_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) : R.scale = k

theorem HCPolySupport.openCubeSet_subset_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) : openCubeSet R ⊆ openCubeSet Q

theorem HCPolySupport.mem_descendantsAtDepth_add_local {d : ℕ} {Q R S : TriadicCube d} {m n : ℕ} (hR : R ∈ descendantsAtDepth Q m) (hS : S ∈ descendantsAtDepth R n) : S ∈ descendantsAtDepth Q (m + n)

theorem HCPolySupport.mem_descendantsAtScale_trans {d : ℕ} {Q R S : TriadicCube d} {k l : ℤ} (hR : R ∈ descendantsAtScale Q k) (hS : S ∈ descendantsAtScale R l) : S ∈ descendantsAtScale Q l

theorem HCPolySupport.OpenCubeDescendantDeterministicCoarseData.of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {a : CoeffField d} {l : ℤ} (hData : OpenCubeDescendantDeterministicCoarseData Q a) (hlQ : l ≤ Q.scale) (hR : R ∈ descendantsAtScale Q l) : OpenCubeDescendantDeterministicCoarseData R a

theorem HCPolySupport.maxDescendantBBlockNormAtScale_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k l : ℤ} (a : CoeffField d) (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantBBlockNormAtScale R l a ≤ maxDescendantBBlockNormAtScale Q l a

theorem HCPolySupport.maxDescendantSigmaStarInvNormAtScale_le_of_mem_descendantsAtScale {d : ℕ} {Q R : TriadicCube d} {k l : ℤ} (a : CoeffField d) (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) : maxDescendantSigmaStarInvNormAtScale R l a ≤ maxDescendantSigmaStarInvNormAtScale Q l a