High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.GaugeFamilyTransfer

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

theorem HCPolySupport.HighContrast.normalizedRoot_centered_conjugation {d : ℕ} [NeZero d] {abar A : Mat d} (hS : Matrix.PosDef (symmPart abar)) : (Selection.normalizedRoot (symmPart abar))⁻¹ * specBound (symmPart abar)⁻¹ • A * matTranspose (Selection.normalizedRoot (symmPart abar))⁻¹ = (matSqrt (symmPart abar))⁻¹ * A * matTranspose (matSqrt (symmPart abar))⁻¹

Projective normalization cancels between the two inverse affine factors and the centered coefficient.

theorem HCPolySupport.HighContrast.exactGaugeCoeff_ae {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (Q : TriadicCube d) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (R : TriadicCube d), (aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) : (aRef.coeffOn Q).toCoeffField =ᵐ[MeasureTheory.volume] fun (y : Vec d) => (matSqrt (symmPart abar))⁻¹ * (↑↑a (matVecMul (Selection.normalizedRoot (symmPart abar)) y) - skewPart abar) * matTranspose (matSqrt (symmPart abar))⁻¹

The certificate family in normalized-root coordinates is the literal square-root-gauge coefficient almost everywhere.

theorem HCPolySupport.HighContrast.matSqrt_physicalGradient_pullback_ae {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (aRef : Book.Ch03.CoeffFamily d) (hCauchy : FiniteAffineCorrectionLocalCauchy aRef) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d) (e : Vec d) (hpullback : (fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (e + gradPhi e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y))) =ᵐ[MeasureTheory.volume] fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) e + (finiteAffineCorrectionJointLocalLimit aRef hCauchy (matVecMul (Selection.normalizedRoot (symmPart abar)) e)).globalGradientRepresentative y) : (fun (y : Vec d) => matVecMul (matSqrt (symmPart abar)) (gradPhi e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y))) =ᵐ[MeasureTheory.volume] (finiteAffineCorrectionJointLocalLimit aRef hCauchy (matVecMul (matSqrt (symmPart abar)) e)).globalGradientRepresentative

Homogeneity of the canonical joint limit cancels the projective scalar in the physical-gradient pullback.

theorem HCPolySupport.HighContrast.physicalFlux_pullback_ae {d : ℕ} [NeZero d] {a : CoeffSpace d} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (Q : TriadicCube d) (aRef : Book.Ch03.CoeffFamily d) (haRef : ∀ (R : TriadicCube d), (aRef.coeffOn R).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯ ↑↑(normalizedCenteredCoeff a abar hS)) (hCauchy : FiniteAffineCorrectionLocalCauchy aRef) (gradPhi : Vec d → CoeffSpace d → Vec d → Vec d) (e : Vec d) (hpullback : (fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) (e + gradPhi e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y))) =ᵐ[MeasureTheory.volume] fun (y : Vec d) => matVecMul (Selection.normalizedRoot (symmPart abar)) e + (finiteAffineCorrectionJointLocalLimit aRef hCauchy (matVecMul (Selection.normalizedRoot (symmPart abar)) e)).globalGradientRepresentative y) : (fun (y : Vec d) => matVecMul (matSqrt (symmPart abar))⁻¹ (matVecMul (↑↑a (matVecMul (Selection.normalizedRoot (symmPart abar)) y) - skewPart abar) (e + gradPhi e a (matVecMul (Selection.normalizedRoot (symmPart abar)) y)) - matVecMul (symmPart abar) e)) =ᵐ[MeasureTheory.volume] fun (y : Vec d) => matVecMul ((aRef.coeffOn Q).toCoeffField y) (matVecMul (matSqrt (symmPart abar)) e + (finiteAffineCorrectionJointLocalLimit aRef hCauchy (matVecMul (matSqrt (symmPart abar)) e)).globalGradientRepresentative y) - matVecMul (matSqrt (symmPart abar)) e

The physical skew-centered flux row pulls back to the identity-reference flux row of the same canonical joint corrector.

def HCPolySupport.HighContrast.closedEuclideanBall (d : ℕ) (r : ℝ) : Set (Vec d)

The exact normalized-root inverse image of the physical ellipsoid.

Equations

• HCPolySupport.HighContrast.closedEuclideanBall d r = {y : HCPolySupport.Vec d | HCPolySupport.vecNormSq y ≤ r ^ 2}

theorem HCPolySupport.HighContrast.measurableSet_closedEuclideanBall (d : ℕ) (r : ℝ) : MeasurableSet (closedEuclideanBall d r)

theorem HCPolySupport.HighContrast.euclideanBall_subset_closedEuclideanBall {d : ℕ} {r : ℝ} : euclideanBall d r ⊆ closedEuclideanBall d r

theorem HCPolySupport.HighContrast.closedEuclideanBall_subset_euclideanBall_two_mul {d : ℕ} {r : ℝ} (hr : 0 < r) : closedEuclideanBall d r ⊆ euclideanBall d (2 * r)

theorem HCPolySupport.HighContrast.closedEuclideanBall_subset_outerCube {d : ℕ} {r : ℝ} (hr : 0 < r) : closedEuclideanBall d r ⊆ openCubeSet (originCube d (outerTriadicGeneration (4 * r) ⋯))

theorem HCPolySupport.HighContrast.volume_closedEuclideanBall_pos {d : ℕ} {r : ℝ} (hr : 0 < r) : 0 < MeasureTheory.volume (closedEuclideanBall d r)

theorem HCPolySupport.HighContrast.volume_closedEuclideanBall_lt_top {d : ℕ} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (closedEuclideanBall d r) < ⊤

theorem HCPolySupport.HighContrast.outerCube_volume_ratio_lt_closedBall {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (openCubeSet (originCube d (outerTriadicGeneration (4 * r) ⋯)))).toReal / (MeasureTheory.volume (closedEuclideanBall d r)).toReal < (6 * √↑d) ^ d

noncomputable def HCPolySupport.HighContrast.closedBallScaledNegOneConstant (d : ℕ) : ℝ

Dimension-dependent prefactor 12 * sqrt ((6 * sqrt d) ^ d) for the scaled negative-order comparison.

Equations

• HCPolySupport.HighContrast.closedBallScaledNegOneConstant d = 12 * √((6 * √↑d) ^ d)

theorem HCPolySupport.HighContrast.closedBallScaledNegOneConstant_pos (d : ℕ) [NeZero d] : 0 < closedBallScaledNegOneConstant d

theorem HCPolySupport.HighContrast.closedBall_scale_prefactor_le {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) : r⁻¹ * √((MeasureTheory.volume (openCubeSet (originCube d (outerTriadicGeneration (4 * r) ⋯)))).toReal / (MeasureTheory.volume (closedEuclideanBall d r)).toReal) ≤ closedBallScaledNegOneConstant d * (3 ^ outerTriadicGeneration (4 * r) ⋯)⁻¹

theorem HCPolySupport.HighContrast.closedBallScaled_negOne_pair_le_originCube {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) (m : ℤ) (hm : m = outerTriadicGeneration (4 * r) ⋯) (F G : Vec d → Vec d) (hF : MemVectorL2 (openCubeSet (originCube d m)) F) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : ENNReal.ofReal r⁻¹ * (negOneNorm (closedEuclideanBall d r) F + negOneNorm (closedEuclideanBall d r) G) ≤ ENNReal.ofReal (closedBallScaledNegOneConstant d) * (ENNReal.ofReal (3 ^ m)⁻¹ * (negOneNorm (openCubeSet (originCube d m)) F + negOneNorm (openCubeSet (originCube d m)) G))

theorem HCPolySupport.HighContrast.matImage_closedBall_eq_ellipsoid {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : matImage (Selection.normalizedRoot (symmPart abar)) (closedEuclideanBall d r) = ellipsoid abar r

The normalized-root image of the exact closed gauge ball is the physical ellipsoid.

theorem HCPolySupport.HighContrast.physicalScaledPair_le_gaugeOriginCube {d : ℕ} [NeZero d] {abar : Mat d} {r : ℝ} (hS : Matrix.PosDef (symmPart abar)) (hr : 0 < r) (m : ℤ) (hm : m = outerTriadicGeneration (4 * r) ⋯) (P₁ P₂ F G : Vec d → Vec d) (h₁ : (fun (y : Vec d) => P₁ (matVecMul (Selection.normalizedRoot (symmPart abar)) y)) =ᵐ[MeasureTheory.volume] F) (h₂ : (fun (y : Vec d) => P₂ (matVecMul (Selection.normalizedRoot (symmPart abar)) y)) =ᵐ[MeasureTheory.volume] G) (hF : MemVectorL2 (openCubeSet (originCube d m)) F) (hG : MemVectorL2 (openCubeSet (originCube d m)) G) : ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) P₁ + ENNReal.ofReal r⁻¹ * negOneNorm (ellipsoid abar r) P₂ ≤ ENNReal.ofReal (√(h1AffineFactor (Selection.normalizedRoot (symmPart abar))) * closedBallScaledNegOneConstant d) * (ENNReal.ofReal (3 ^ m)⁻¹ * (negOneNorm (openCubeSet (originCube d m)) F + negOneNorm (openCubeSet (originCube d m)) G))

Exact affine transport followed by closed-ball restriction converts a physical inverse-radius pair to the inverse-triadic-scale gauge pair.