High-contrast homogenization: Provider.Regularity.LocalGradientTopology

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

A countable local-gradient topology

Local weak gradients are represented by compatible L² classes on the centered open triadic cubes. The resulting countable projective carrier has the product topology and measurable structure, so measurable finite-volume gradients can be passed to coordinatewise limits without choosing pointwise representatives.

def HCPolySupport.HighContrast.localGradientCube (d n : ℕ) : Set (Vec d)

The nth member of the centered open-cube exhaustion of Vec d.

Equations

• HCPolySupport.HighContrast.localGradientCube d n = HCPolySupport.openCubeSet (HCPolySupport.originCube d ↑n)

theorem HCPolySupport.HighContrast.localGradientCube_mono {d m n : ℕ} (hmn : m ≤ n) : localGradientCube d m ⊆ localGradientCube d n

Centered cubes in the local-gradient exhaustion are nested.

theorem HCPolySupport.HighContrast.iUnion_localGradientCube (d : ℕ) : ⋃ (n : ℕ), localGradientCube d n = Set.univ

The centered cubes exhaust the whole Euclidean space.

@[reducible, inline]

noncomputable abbrev HCPolySupport.HighContrast.LocalGradientL2 (d n : ℕ) : AddSubgroup (Vec d →ₘ[volumeMeasureOn (localGradientCube d n)] HilbertVec d)

Hilbert-valued L² gradients on one member of the exhaustion.

Equations

• HCPolySupport.HighContrast.LocalGradientL2 d n = HCPolySupport.HilbertVectorL2 (HCPolySupport.HighContrast.localGradientCube d n)

noncomputable def HCPolySupport.HighContrast.localGradientRestrictLinear {d m n : ℕ} (hmn : m ≤ n) : ↥(LocalGradientL2 d n) →ₗ[ℝ] ↥(LocalGradientL2 d m)

The real linear restriction of an L² gradient from exhaustion cube n to cube m ≤ n.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.localGradientRestrictLinear_norm_le {d m n : ℕ} (hmn : m ≤ n) (g : ↥(LocalGradientL2 d n)) : ‖(localGradientRestrictLinear hmn) g‖ ≤ ‖g‖

noncomputable def HCPolySupport.HighContrast.localGradientRestrict {d m n : ℕ} (hmn : m ≤ n) : ↥(LocalGradientL2 d n) →L[ℝ] ↥(LocalGradientL2 d m)

Restriction of an L² a.e. class from a larger exhaustion cube to a smaller one.

Equations

• HCPolySupport.HighContrast.localGradientRestrict hmn = (HCPolySupport.HighContrast.localGradientRestrictLinear hmn).mkContinuous 1 ⋯

theorem HCPolySupport.HighContrast.localGradientRestrict_coeFn_ae {d m n : ℕ} (hmn : m ≤ n) (g : ↥(LocalGradientL2 d n)) : ↑↑((localGradientRestrict hmn) g) =ᵐ[volumeMeasureOn (localGradientCube d m)] ↑↑g

Restriction agrees almost everywhere with the same local representative.

theorem HCPolySupport.HighContrast.localGradientRestrict_eq_iff_ae {d m n : ℕ} (hmn : m ≤ n) (g : ↥(LocalGradientL2 d n)) (h : ↥(LocalGradientL2 d m)) : (localGradientRestrict hmn) g = h ↔ ↑↑g =ᵐ[volumeMeasureOn (localGradientCube d m)] ↑↑h

The restricted class is characterized by any representative which agrees with the original class almost everywhere on the smaller cube.

@[simp]

theorem HCPolySupport.HighContrast.localGradientRestrict_refl {d n : ℕ} : localGradientRestrict ⋯ = ContinuousLinearMap.id ℝ ↥(LocalGradientL2 d n)

Restricting to the same cube is the identity.

noncomputable def HCPolySupport.HighContrast.localGradientProjectiveSubmodule (d : ℕ) : Submodule ℝ ((n : ℕ) → ↥(LocalGradientL2 d n))

Compatible local L² classes form the projective local-gradient submodule.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev HCPolySupport.HighContrast.LocalGradientCarrier (d : ℕ) : Submodule ℝ ((n : ℕ) → ↥(LocalGradientL2 d n))

The countable projective carrier for local weak-gradient classes.

Equations

• HCPolySupport.HighContrast.LocalGradientCarrier d = HCPolySupport.HighContrast.localGradientProjectiveSubmodule d

def HCPolySupport.HighContrast.LocalGradientCarrier.component {d : ℕ} (g : ↥(LocalGradientCarrier d)) (n : ℕ) : ↥(LocalGradientL2 d n)

The local L² class on the nth exhaustion cube.

Equations

• HCPolySupport.HighContrast.LocalGradientCarrier.component g n = ↑g n

theorem HCPolySupport.HighContrast.LocalGradientCarrier.restrict_component {d : ℕ} (g : ↥(LocalGradientCarrier d)) {m n : ℕ} (hmn : m ≤ n) : (localGradientRestrict hmn) (component g n) = component g m

Components agree under restriction to every smaller exhaustion cube.

theorem HCPolySupport.HighContrast.LocalGradientCarrier.ext {d : ℕ} {f g : ↥(LocalGradientCarrier d)} (h : ∀ (n : ℕ), component f n = component g n) : f = g

A projective local gradient is determined by its local components.

theorem HCPolySupport.HighContrast.LocalGradientCarrier.ext_iff {d : ℕ} {f g : ↥(LocalGradientCarrier d)} : f = g ↔ ∀ (n : ℕ), component f n = component g n