Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.HodgeCubeBridge

Coarse-graining support: Support.Sobolev.Foundations.HodgeCubeBridge #

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

This file transports the open-cube Hodge converse to the half-open centered cube used by the deterministic multiscale layer.

source
theorem HCPolySupport.memVectorL2_comp_addRight_of_memVectorL2_translateSet {d : ℕ} {U : Set (Vec d)} {z : Vec d} {f : Vec d → Vec d} (hf : MemVectorL2 (translateSet z U) f) :
MemVectorL2 U fun (x : Vec d) => f (x + z)
source
theorem HCPolySupport.memVectorL2_translateSet_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {z : Vec d} {f : Vec d → Vec d} (hf : MemVectorL2 U f) :
MemVectorL2 (translateSet z U) fun (x : Vec d) => f (x - z)
source
theorem HCPolySupport.hodgeConverseCriterion_translateSet {d : ℕ} {U : Set (Vec d)} (z : Vec d) (hHodge : HodgeConverseCriterion U) :
HodgeConverseCriterion (translateSet z U)

The Hodge converse is invariant under translating the domain.

source
theorem HCPolySupport.hodgeConverseCriterion_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} :
HodgeConverseCriterion (cubeSet (originCube d n))

The half-open centered cube satisfies the Hodge converse because it agrees almost everywhere with the corresponding open centered cube, and the latter is a bounded open convex domain.

source
theorem HCPolySupport.hasHodgeConverse_cubeSet_originCube {d : ℕ} [NeZero d] {n : ℤ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet (originCube d n)))] :
HasHodgeConverse (cubeSet (originCube d n))

Packaged centered half-open cube Hodge converse.

source
theorem HCPolySupport.hodgeConverseCriterion_cubeSet_triadicCube {d : ℕ} [NeZero d] (Q : TriadicCube d) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))] :
HodgeConverseCriterion (cubeSet Q)

Every half-open triadic cube satisfies the Hodge converse.

source
theorem HCPolySupport.hasHodgeConverse_cubeSet_triadicCube {d : ℕ} [NeZero d] (Q : TriadicCube d) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))] :
HasHodgeConverse (cubeSet Q)

Packaged Hodge converse on every half-open triadic cube.

source
instance HCPolySupport.instHasHodgeConverseCubeSet {d : ℕ} [NeZero d] (Q : TriadicCube d) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn (cubeSet Q))] :
HasHodgeConverse (cubeSet Q)