Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarsePoincare.Setup.HarmonicAndData

Coarse-graining support: Support.Deterministic.CoarsePoincare.Setup.HarmonicAndData #

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

source
theorem HCPolySupport.cubeAverageFlux_le_coarseBBlockNorm_mul_energyAverage_of_of_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a)) (hS : IsSigmaStarCoarse (openCubeSet R) a sigmaStar) (hK : IsKappaCoarse (openCubeSet R) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet R) a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) ≤ coarseBBlockNorm R a * cubeAverage R (scalarVariationEnergyIntegrand a w)
source
theorem HCPolySupport.cubeAverageFlux_le_matrixNorm_bCoarse_mul_energyAverage_of_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a)) (hS : IsSigmaStarCoarse (openCubeSet R) a sigmaStar) (hK : IsKappaCoarse (openCubeSet R) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet R) a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) ≤ Book.Ch02.matrixNorm (bCoarse (sigmaCoarse (cubeSet R) a) (sigmaStarCoarse (cubeSet R) a) (kappaCoarse (cubeSet R) a)) * cubeAverage R (scalarVariationEnergyIntegrand a w)
source
theorem HCPolySupport.cubeAverageFlux_le_coarseBBlockNorm_mul_energyAverage_of_ellipticField {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) (hData : OpenCubeDeterministicCoarseData R a) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) ≤ coarseBBlockNorm R a * cubeAverage R (scalarVariationEnergyIntegrand a w)

Flux coarse-square estimate with the deterministic open-cube coarse witnesses packaged as OpenCubeDeterministicCoarseData.

source
theorem HCPolySupport.cubeAverageFlux_le_matrixNorm_bCoarse_mul_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) (hData : OpenCubeDeterministicCoarseData R a) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => matVecMul (a x) (w.toH1.grad x)) ≤ Book.Ch02.matrixNorm (bCoarse (sigmaCoarse (cubeSet R) a) (sigmaStarCoarse (cubeSet R) a) (kappaCoarse (cubeSet R) a)) * cubeAverage R (scalarVariationEnergyIntegrand a w)
source
theorem HCPolySupport.cubeAverageGradient_le_coarseSigmaStarInvBlockNorm_mul_of_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a)) (hS : IsSigmaStarCoarse (openCubeSet R) a sigmaStar) (hK : IsKappaCoarse (openCubeSet R) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet R) a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => w.toH1.grad x) ≤ coarseSigmaStarInvBlockNorm R a * cubeAverage R (scalarVariationEnergyIntegrand a w)
source
theorem HCPolySupport.cubeAverageGradient_le_matrixNorm_sigmaStarInv_mul_of_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) {sigma sigmaStar kappa : Mat d} (_hA : IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a)) (hS : IsSigmaStarCoarse (openCubeSet R) a sigmaStar) (hK : IsKappaCoarse (openCubeSet R) a sigmaStar kappa) (hSigma : IsSigmaCoarse (openCubeSet R) a sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => w.toH1.grad x) ≤ Book.Ch02.matrixNorm (sigmaStarInvCoarse (cubeSet R) a) * cubeAverage R (scalarVariationEnergyIntegrand a w)
source
theorem HCPolySupport.cubeAverageGradient_le_coarseSigmaStarInvBlockNorm_mul_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) (hData : OpenCubeDeterministicCoarseData R a) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => w.toH1.grad x) ≤ coarseSigmaStarInvBlockNorm R a * cubeAverage R (scalarVariationEnergyIntegrand a w)

Gradient coarse-square estimate with the deterministic open-cube coarse witnesses packaged as OpenCubeDeterministicCoarseData.

source
theorem HCPolySupport.cubeAverageGradient_le_matrixNorm_sigmaStarInv_mul_energyAverage {d : ℕ} [NeZero d] (R : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet R) a) (hData : OpenCubeDeterministicCoarseData R a) (w : AHarmonicFunction a (cubeSet R)) :
vecNormSq (cubeAverageVec R fun (x : Vec d) => w.toH1.grad x) ≤ Book.Ch02.matrixNorm (sigmaStarInvCoarse (cubeSet R) a) * cubeAverage R (scalarVariationEnergyIntegrand a w)
source
theorem HCPolySupport.cubeAverageGradientEnergyControl_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => u.toH1.grad x) fun (x : Vec d) => scalarVariationEnergyIntegrand a u x
source
theorem HCPolySupport.cubeAverageGradientEnergyControl_of_harmonic_descendantRecovery {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => u.toH1.grad x) fun (x : Vec d) => scalarVariationEnergyIntegrand a u x
source
theorem HCPolySupport.harmonicGradientEnergy_le_scalarVariation_of_recovery {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) :
CubeAverageGradientEnergyControl Q a (fun (x : Vec d) => u.toH1.grad x) fun (x : Vec d) => scalarVariationEnergyIntegrand a u x
source
theorem HCPolySupport.mem_descendantsAtScale_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) :
R ∈ descendantsAtScale Q (Q.scale - ↑j)
source
theorem HCPolySupport.cubeAverageFluxEnergyControl_of_aHarmonicFunction {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) (hData : OpenCubeDescendantDeterministicCoarseData Q a) :
CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a u x
source
theorem HCPolySupport.cubeAverageFluxEnergyControl_of_aHarmonicFunction_of_openCubeDescendantEllipticRecoveryFamily {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) (hRec : OpenCubeDescendantEllipticRecoveryFamily Q a) :
CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a u x
source
theorem HCPolySupport.cubeAverageFluxEnergyControl_of_aHarmonicFunction_of_openCubeOriginEllipticRecoveryExistence {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (u : AHarmonicFunction a (cubeSet Q)) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) :
CubeAverageFluxEnergyControl Q a (fun (x : Vec d) => matVecMul (a x) (u.toH1.grad x)) fun (x : Vec d) => scalarVariationEnergyIntegrand a u x
source
theorem HCPolySupport.rpow_neg_s_nat_eq_inv_geometricDiscount_mul_geometricWeight {s : ℝ} (hs : 0 < s) (j : ℕ) :
Real.rpow 3 (-s * ↑j) = (geometricDiscount s 1)⁻¹ * geometricWeight s 1 j
source
theorem HCPolySupport.mul_sqrt_mul_eq_mul_rpow_half_mul_sqrt {a b c : ℝ} (ha : 0 ≤ a) :
c * √(a * b) = c * a.rpow (1 / 2) * √b