Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.Theorems.PublicInternalBridges.CoeffField

Coarse-graining support: Support.Book.Ch03.Theorems.PublicInternalBridges.CoeffField #

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

Public coefficient-field bridges for Chapter 3 #

This file contains the pointwise coefficient representative, descendant-data bridges, Ch2 multiscale translations, and homogenization-error translations used by the broader Chapter 3 public/internal bridge layer.

@[reducible, inline]

noncomputable abbrev HCPolySupport.Book.Ch03.publicCoeffField {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) :

Pointwise representative of the public coefficient family on Q.

It is a.e. equal to the public CoeffOn field on the open cube, but is pointwise elliptic on every descendant cube, making it suitable for the deterministic coarse-graining APIs.

Equations

HCPolySupport.Book.Ch03.publicCoeffField Q a = HCPolySupport.Internal.Ch02.BookCh02.pointwiseCoeffField (HCPolySupport.Book.Ch02.cubeDomain Q) (a.coeffOn Q)

Instances For

theorem HCPolySupport.Book.Ch03.publicCoeffField_ae_eq {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) :

publicCoeffField Q a =ᵐ[volumeMeasureOn (Ch02.cubeDomain Q).carrier] (a.coeffOn Q).toCoeffField

theorem HCPolySupport.Book.Ch03.publicCoeffField_ae_eq_openCubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) :

publicCoeffField Q a =ᵐ[volumeMeasureOn (openCubeSet Q)] (a.coeffOn Q).toCoeffField

theorem HCPolySupport.Book.Ch03.publicCoeffField_ae_eq_cubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) :

publicCoeffField Q a =ᵐ[volumeMeasureOn (cubeSet Q)] (a.coeffOn Q).toCoeffField

theorem HCPolySupport.Book.Ch03.publicCoeffField_isEllipticFieldOn {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) :

IsEllipticFieldOn (a.coeffOn Q).lam (a.coeffOn Q).Lam (Ch02.cubeDomain Q).carrier (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_isEllipticFieldOn_openCubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) :

IsEllipticFieldOn (a.coeffOn Q).lam (a.coeffOn Q).Lam (openCubeSet Q) (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_isEllipticFieldOn_cubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) :

IsEllipticFieldOn (a.coeffOn Q).lam (a.coeffOn Q).Lam (cubeSet Q) (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_isEllipticFieldOn_descendant_openCubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :

IsEllipticFieldOn (a.coeffOn Q).lam (a.coeffOn Q).Lam (openCubeSet R) (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_isEllipticFieldOn_descendant_cubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :

IsEllipticFieldOn (a.coeffOn Q).lam (a.coeffOn Q).Lam (cubeSet R) (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_openCubeDescendantDeterministicCoarseData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) :

OpenCubeDescendantDeterministicCoarseData Q (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_openCubeDeterministicCoarseData {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) :

OpenCubeDeterministicCoarseData Q (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_openCubeDescendantDeterministicCoarseData_descendant {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :

OpenCubeDescendantDeterministicCoarseData R (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_openCubeDeterministicCoarseData_descendant {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :

OpenCubeDeterministicCoarseData R (publicCoeffField Q a)

noncomputable def HCPolySupport.Book.Ch03.h1CoerciveEstimateCubeSet {d : ℕ} (Q : TriadicCube d) :

H1CoerciveEstimate (cubeSet Q)

The H¹ coercive estimate on the closed triadic cube.

Equations

HCPolySupport.Book.Ch03.h1CoerciveEstimateCubeSet Q = HCPolySupport.cubeSetH1CoerciveEstimate Q

Instances For

theorem HCPolySupport.Book.Ch03.publicCoeffField_summable_qtwo_maxDescendantBBlockNormAtScale {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} (hs : 0 < s) :

Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_summable_qtwo_maxDescendantBBlockNormAtScale_rpow_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} (hs : 0 < s) :

Summable fun (n : ℕ) => geometricWeight s 2 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) (publicCoeffField Q a)).rpow 1

theorem HCPolySupport.Book.Ch03.publicCoeffField_summable_qtwo_maxDescendantBBlockNormAtScale_descendant {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) {s : ℝ} (hs : 0 < s) :

Summable fun (n : ℕ) => geometricWeight s 2 n * maxDescendantBBlockNormAtScale R (R.scale - ↑n) (publicCoeffField Q a)

theorem HCPolySupport.Book.Ch03.publicCoeffField_summable_qtwo_maxDescendantBBlockNormAtScale_descendant_rpow_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) {s : ℝ} (hs : 0 < s) :

Summable fun (n : ℕ) => geometricWeight s 2 n * (maxDescendantBBlockNormAtScale R (R.scale - ↑n) (publicCoeffField Q a)).rpow 1

theorem HCPolySupport.Book.Ch03.publicCoeffField_ae_eq_descendant_openCubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :

publicCoeffField Q a =ᵐ[volumeMeasureOn (openCubeSet R)] (a.coeffOn R).toCoeffField

theorem HCPolySupport.Book.Ch03.publicCoeffField_ae_eq_descendant_cubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :

publicCoeffField Q a =ᵐ[volumeMeasureOn (cubeSet R)] (a.coeffOn R).toCoeffField

theorem HCPolySupport.Book.Ch03.publicCoeffField_ae_eq_publicCoeffField_descendant_cubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffFamily d) {R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :

publicCoeffField Q a =ᵐ[volumeMeasureOn (cubeSet R)] publicCoeffField R a

theorem HCPolySupport.Book.Ch03.memVectorL2_cubeSet_of_forceBesovRegularity {d : ℕ} {Q : TriadicCube d} {s : ℝ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q s g) :

MemVectorL2 (cubeSet Q) g

theorem HCPolySupport.Book.Ch03.memVectorL2_descendant_cubeSet_of_forceBesovRegularity {d : ℕ} {Q R : TriadicCube d} {s : ℝ} {j : ℕ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q s g) (hR : R ∈ descendantsAtDepth Q j) :

MemVectorL2 (cubeSet R) g

theorem HCPolySupport.Book.Ch03.forceBesovRegularity_descendant_memLp_normalizedCubeMeasure {d : ℕ} {Q R : TriadicCube d} {s : ℝ} {j : ℕ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q s g) (hR : R ∈ descendantsAtDepth Q j) :

MeasureTheory.MemLp g 2 (normalizedCubeMeasure R)

theorem HCPolySupport.Book.Ch03.forceBesovRegularity_descendant_partialSeminorms_bddAbove {d : ℕ} {Q R : TriadicCube d} {s : ℝ} {j : ℕ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q s g) (hR : R ∈ descendantsAtDepth Q j) :

BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N g)

theorem HCPolySupport.Book.Ch03.forceBesovRegularity_descendant_centered_partialSeminorms_bddAbove {d : ℕ} {Q R : TriadicCube d} {s : ℝ} {j : ℕ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q s g) (hR : R ∈ descendantsAtDepth Q j) :

BddAbove (Set.range fun (N : ℕ) => cubeBesovPositiveVectorPartialSeminormTwo R s N fun (x : Vec d) => g x - cubeAverageVec R g)

theorem HCPolySupport.Book.Ch03.forceBesovRegularity_descendant {d : ℕ} {Q R : TriadicCube d} {s : ℝ} {j : ℕ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q s g) (hR : R ∈ descendantsAtDepth Q j) :

ForceBesovRegularity R s g

theorem HCPolySupport.Book.Ch03.forceBesovRegularity_negativeBesovPartialSeminormTwo_bddAbove {d : ℕ} {Q : TriadicCube d} {s t : ℝ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q t g) (hs : 0 < s) :

BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo Q s N g)

theorem HCPolySupport.Book.Ch03.forceBesovRegularity_descendant_negativeBesovPartialSeminormTwo_bddAbove {d : ℕ} {Q R : TriadicCube d} {s t : ℝ} {j : ℕ} {g : Vec d → Vec d} (hg : ForceBesovRegularity Q t g) (hR : R ∈ descendantsAtDepth Q j) (hs : 0 < s) :

BddAbove (Set.range fun (N : ℕ) => cubeBesovNegativeVectorPartialSeminormTwo R s N g)

theorem HCPolySupport.Book.Ch03.constantCoeffMatrix_isEllipticFieldOn_constantCoeffField {d : ℕ} {U : Set (Vec d)} (a0 : ConstantCoeffMatrix d) (hU : MeasurableSet U) :

IsEllipticFieldOn a0.lam a0.Lam U (constantCoeffField a0.matrix)

theorem HCPolySupport.Book.Ch03.matNorm_le_dim_mul_constantCoeffMatrixNorm {d : ℕ} (a0 : ConstantCoeffMatrix d) :

matNorm a0.matrix ≤ ↑d * constantCoeffMatrixNorm a0

theorem HCPolySupport.Book.Ch03.sqrt_matNorm_le_dim_mul_constantCoeffMatrixNormHalf {d : ℕ} [NeZero d] (a0 : ConstantCoeffMatrix d) :

√(matNorm a0.matrix) ≤ ↑d * constantCoeffMatrixNormHalf a0

theorem HCPolySupport.Book.Ch03.sqrt_LambdaSq_publicCoeffField_finite_one_le_dim_mul_poincareUpperEllipticityFactor {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} (hs : 0 < s) :

√(LambdaSq Q s (MultiscaleExponent.finite 1) (publicCoeffField Q a)) ≤ ↑d * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 1)

theorem HCPolySupport.Book.Ch03.sqrt_lambdaSq_publicCoeffField_finite_one_inv_le_dim_mul_poincareLowerEllipticityFactor {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} (hs : 0 < s) :

√(lambdaSq Q s (MultiscaleExponent.finite 1) (publicCoeffField Q a))⁻¹ ≤ ↑d * poincareLowerEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 1)

theorem HCPolySupport.Book.Ch03.sqrt_LambdaSq_publicCoeffField_finite_two_le_dim_mul_poincareUpperEllipticityFactor {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} (hs : 0 < s) :

√(LambdaSq Q s (MultiscaleExponent.finite 2) (publicCoeffField Q a)) ≤ ↑d * poincareUpperEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2)

theorem HCPolySupport.Book.Ch03.sqrt_lambdaSq_publicCoeffField_finite_two_inv_le_dim_mul_poincareLowerEllipticityFactor {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} (hs : 0 < s) :

√(lambdaSq Q s (MultiscaleExponent.finite 2) (publicCoeffField Q a))⁻¹ ≤ ↑d * poincareLowerEllipticityFactor Q a s (Ch02.MultiscaleExponent.finite 2)

theorem HCPolySupport.Book.Ch03.lambdaSq_publicCoeffField_finite_two_inv_le_dim_mul_public_rpow_neg_one {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffFamily d) {s : ℝ} (hs : 0 < s) :

(lambdaSq Q s (MultiscaleExponent.finite 2) (publicCoeffField Q a))⁻¹ ≤ ↑d * (Ch02.lambdaSq Q s (Ch02.MultiscaleExponent.finite 2) a).rpow (-1)

theorem HCPolySupport.Book.Ch03.blockJ_cubeSet_publicCoeffField_eq_ch02_doubledResponseJ {d : ℕ} [NeZero d] (a : CoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) (P Q' : BlockVec d) :

BlockJ (cubeSet R) P Q' (publicCoeffField Q a) = Ch02.doubledResponseJ (Ch02.cubeDomain R) (a.coeffOn R) P Q'

theorem HCPolySupport.Book.Ch03.normalizedBlockResponseValueSet_publicCoeffField_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) (a0 : Mat d) :

normalizedBlockResponseValueSet R (publicCoeffField Q a) a0 = Ch02.normalizedBlockResponseValueSet R a a0

theorem HCPolySupport.Book.Ch03.normalizedBlockResponseMax_publicCoeffField_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hk : k ≤ Q.scale) (hR : R ∈ descendantsAtScale Q k) (a0 : Mat d) :

normalizedBlockResponseMax R (publicCoeffField Q a) a0 = Ch02.normalizedBlockResponseMax R a a0

theorem HCPolySupport.Book.Ch03.maxDescendantNormalizedBlockResponseAtScale_publicCoeffField_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a0 : Mat d) :

maxDescendantNormalizedBlockResponseAtScale Q k (publicCoeffField Q a) a0 = Ch02.maxDescendantNormalizedBlockResponseAtScale Q k a a0

theorem HCPolySupport.Book.Ch03.scaleResponseAtScale_publicCoeffField_infinity_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) (Q : TriadicCube d) {k : ℤ} (hk : k ≤ Q.scale) (a0 : Mat d) :

scaleResponseAtScale Q k MultiscaleExponent.infinity (publicCoeffField Q a) a0 = Ch02.scaleResponseAtScale Q k Ch02.MultiscaleExponent.infinity a a0

theorem HCPolySupport.Book.Ch03.maxDescendantNormalizedBlockResponseAtScale_parent_publicCoeffField_descendant_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) {Q R : TriadicCube d} {k l : ℤ} (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) (a0 : Mat d) :

maxDescendantNormalizedBlockResponseAtScale R l (publicCoeffField Q a) a0 = Ch02.maxDescendantNormalizedBlockResponseAtScale R l a a0

theorem HCPolySupport.Book.Ch03.scaleResponseAtScale_parent_publicCoeffField_descendant_infinity_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) {Q R : TriadicCube d} {k l : ℤ} (hR : R ∈ descendantsAtScale Q k) (hl : l ≤ R.scale) (a0 : Mat d) :

scaleResponseAtScale R l MultiscaleExponent.infinity (publicCoeffField Q a) a0 = Ch02.scaleResponseAtScale R l Ch02.MultiscaleExponent.infinity a a0

theorem HCPolySupport.Book.Ch03.homogenizationErrorOnCube_parent_publicCoeffField_descendant_infinity_one_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) (s : ℝ) (a0 : Mat d) :

HomogenizationErrorOnCube R s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) (publicCoeffField Q a) a0 = Ch02.HomogenizationErrorOnCube R s Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.Book.Ch03.homogenizationErrorOnCube_parent_publicCoeffField_descendant_infinity_one_terms_summable {d : ℕ} [NeZero d] (a : CoeffFamily d) {Q R : TriadicCube d} {k : ℤ} (hR : R ∈ descendantsAtScale Q k) (a0 : Mat d) {s : ℝ} (hs : 0 < s) :

Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale R (R.scale - ↑n) MultiscaleExponent.infinity (publicCoeffField Q a) a0

theorem HCPolySupport.Book.Ch03.homogenizationErrorOnCube_publicCoeffField_infinity_one_eq_ch02 {d : ℕ} [NeZero d] (a : CoeffFamily d) (Q : TriadicCube d) (s : ℝ) (a0 : Mat d) :

HomogenizationErrorOnCube Q s MultiscaleExponent.infinity (MultiscaleExponent.finite 1) (publicCoeffField Q a) a0 = Ch02.HomogenizationErrorOnCube Q s Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite 1) a a0

theorem HCPolySupport.Book.Ch03.homogenizationErrorOnCube_publicCoeffField_infinity_one_terms_summable {d : ℕ} [NeZero d] (a : CoeffFamily d) (Q : TriadicCube d) (a0 : Mat d) {s : ℝ} (hs : 0 < s) :

Summable fun (n : ℕ) => geometricWeight s 1 n * scaleResponseAtScale Q (Q.scale - ↑n) MultiscaleExponent.infinity (publicCoeffField Q a) a0