Import high-contrast stochastic homogenization

LeanPool/HighContrastHomogenization.lean

@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Scott Armstrong, Tuomo Kuusi, Amélie Loher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong, Tuomo Kuusi, Amélie Loher
+-/
+
+module
+
+-- Project aggregator: the frozen exports (each pulls in exactly its provider
+-- chain) and the consistency checks of the definitions, which no export imports.
+public import LeanPool.HighContrastHomogenization.Analytic
+public import LeanPool.HighContrastHomogenization.Annealed.Witness
+public import LeanPool.HighContrastHomogenization.Basic
+public import LeanPool.HighContrastHomogenization.Consistency
+public import LeanPool.HighContrastHomogenization.Frozen.CoarseEllipticityDagger
+public import LeanPool.HighContrastHomogenization.Frozen.PolynomialEntry
+public import LeanPool.HighContrastHomogenization.Frozen.PolynomialEntryBridge
+public import LeanPool.HighContrastHomogenization.Frozen.PolynomialHomogenization
+public import LeanPool.HighContrastHomogenization.Frozen.QuenchedConvergence
+public import LeanPool.HighContrastHomogenization.Frozen.Stationarity
+public import LeanPool.HighContrastHomogenization.Frozen.UnitRange
+public import LeanPool.HighContrastHomogenization.MainResults
+
+-- The polynomial-entry route: the sixteen printed propositions whose statements the
+-- entry theorem is assembled from, and the three statements carried in
+-- CoarseGraining's own vocabulary.  `HCPoly.Entry.Statements.PolynomialEntry` itself
+-- arrives through `HCPoly.Frozen.PolynomialEntryBridge`.
+public import LeanPool.HighContrastHomogenization.Entry.CG.Anchors.ResponseFiniteDefect
+public import LeanPool.HighContrastHomogenization.Entry.CG.Anchors.ResponseSubadditiveCountable
+public import LeanPool.HighContrastHomogenization.Entry.CG.Anchors.ResponseSummable
+public import LeanPool.HighContrastHomogenization.Entry.Statements.GlobalSelection
+public import LeanPool.HighContrastHomogenization.Entry.Statements.InitialFixedGridScale
+public import LeanPool.HighContrastHomogenization.Entry.Statements.MatrixAveraging
+public import LeanPool.HighContrastHomogenization.Entry.Statements.OneGridPropagation
+public import LeanPool.HighContrastHomogenization.Entry.Statements.ParentChildRecurrence
+public import LeanPool.HighContrastHomogenization.Entry.Statements.PositiveGap
+public import LeanPool.HighContrastHomogenization.Entry.Statements.ProjectiveStep
+public import LeanPool.HighContrastHomogenization.Entry.Statements.ResponseTransfer
+public import LeanPool.HighContrastHomogenization.Entry.Statements.ScaleSelection
+public import LeanPool.HighContrastHomogenization.Entry.Statements.SourceWhitney
+public import LeanPool.HighContrastHomogenization.Entry.Statements.SuccessfulShortBridge
+public import LeanPool.HighContrastHomogenization.Entry.Statements.TwoGridTransport
+public import LeanPool.HighContrastHomogenization.Entry.Statements.TwoGridWhitney
+
+/-!
+# Homogenization at a polynomial scale in high contrast
+
+Source: arxiv:2609.27647, url:https://github.com/scottnarmstrong/HighContrastHomogenization/tree/7a13dbcd8d6609264a713373f5c69ceeac870472
+Authors: Scott Armstrong, Tuomo Kuusi, Amélie Loher
+Status: verified
+Main declarations: `HCPoly.polynomial_homogenization`
+Tags: homogenization, elliptic-equations, probability, high-contrast
+MSC: 35B27, 35J15, 60K37
+-/
+
+public section

LeanPool/HighContrastHomogenization/Analytic.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Scott Armstrong, Tuomo Kuusi, Amélie Loher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong, Tuomo Kuusi, Amélie Loher
+-/
+
+module
+
+public import LeanPool.HighContrastHomogenization.Analytic.EuclideanAmbient
+public import LeanPool.HighContrastHomogenization.Analytic.ConvexDomains
+public import LeanPool.HighContrastHomogenization.Analytic.NormComparison
+public import LeanPool.HighContrastHomogenization.Analytic.SingularKernel
+public import LeanPool.HighContrastHomogenization.Analytic.TestNorms
+public import LeanPool.HighContrastHomogenization.Analytic.EllipsoidGeometry
+public import LeanPool.HighContrastHomogenization.Analytic.AntiVacuityInstances
+public import LeanPool.HighContrastHomogenization.Analytic.DualNormJunk
+public import LeanPool.HighContrastHomogenization.Analytic.CenteringInvariance
+public import LeanPool.HighContrastHomogenization.Analytic.WeakPairing
+public import LeanPool.HighContrastHomogenization.Analytic.WeightedEnergy
+public import LeanPool.HighContrastHomogenization.Analytic.ClassHonesty
+public import LeanPool.HighContrastHomogenization.Analytic.ClassCounterexample
+public import LeanPool.HighContrastHomogenization.Analytic.ClassPairing
+public import LeanPool.HighContrastHomogenization.Analytic.LocalIntegrability
+public import LeanPool.HighContrastHomogenization.Analytic.WeakGradientClosure
+public import LeanPool.HighContrastHomogenization.Analytic.ClosureH1a
+public import LeanPool.HighContrastHomogenization.Analytic.DirichletDomain
+public import LeanPool.HighContrastHomogenization.Analytic.NormEquivalence
+public import LeanPool.HighContrastHomogenization.Analytic.ScaledCoeff
+
+/-!
+# High-contrast homogenization: Analytic
+
+Imported from the Apache-2.0 HighContrastHomogenization development at commit
+`7a13dbcd8d6609264a713373f5c69ceeac870472`.
+-/
+
+public section
+
+/-!
+# The analytic provider layer for the homogenization theorem
+
+The proofs standing behind the conclusion of
+`t.random.homogenization`: the fail-closed behaviour of the
+normalized dual norms, the convex domains and the shape datum carried by the
+Dirichlet estimate, the weighted Sobolev classes and the absolute convergence of
+their pairings, and the membership classes they are read on.
+
+These modules sit below the frozen statement and are imported by no frozen file,
+so they may be extended without moving any frozen declaration's pin.
+-/

LeanPool/HighContrastHomogenization/Analytic/AffineFields.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Scott Armstrong, Tuomo Kuusi, Amélie Loher. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Armstrong, Tuomo Kuusi, Amélie Loher
+-/
+
+module
+
+public import LeanPool.HighContrastHomogenization.Analytic.CenteringInvariance
+public import LeanPool.HighContrastHomogenization.Analytic.DirichletDomain
+
+/-!
+# High-contrast homogenization: Analytic.AffineFields
+
+Imported from the Apache-2.0 HighContrastHomogenization development at commit
+`7a13dbcd8d6609264a713373f5c69ceeac870472`.
+-/
+
+public section
+
+/-!
+# Fields in the symmetric affine normalization
+
+The symmetric square-root change of variables sends physical gradients and
+skew-centered fluxes to the two fields used by the deterministic comparison.
+-/
+
+namespace HCPolySupport
+namespace HighContrast
+
+noncomputable section
+
+variable {d : ℕ}
+
+/-- The square-root map carries a gradient difference to the difference of
+the transformed gradients. -/
+theorem matSqrt_gradient_difference_eq (S : Mat d) (F G : Vec d) :
+    matVecMul (matSqrt S) F - matVecMul (matSqrt S) G =
+      matVecMul (matSqrt S) (F - G) := by
+  funext i
+  simp only [Pi.sub_apply, matVecMul, mul_sub, Finset.sum_sub_distrib]
+
+/-- Inverse-square-root congruence carries the centered flux difference to
+the normalized flux difference. -/
+theorem matSqrt_inv_centered_flux_difference_eq {S A : Mat d}
+    (hS : S.PosDef) (F G : Vec d) :
+    matVecMul ((matSqrt S)⁻¹ * A * matTranspose (matSqrt S)⁻¹)
+          (matVecMul (matSqrt S) F) - matVecMul (matSqrt S) G =
+      matVecMul (matSqrt S)⁻¹
+        (matVecMul A F - matVecMul S G) := by
+  have hUnit : IsUnit (matSqrt S).det := isUnit_det_matSqrt hS
+  have hSymm : matTranspose (matSqrt S)⁻¹ = (matSqrt S)⁻¹ := by
+    rw [← matSqrt_inv hS]
+    exact transpose_matSqrt_inv hS
+  have hLeft :
+      matVecMul ((matSqrt S)⁻¹ * A * matTranspose (matSqrt S)⁻¹)
+          (matVecMul (matSqrt S) F) =
+        matVecMul (matSqrt S)⁻¹ (matVecMul A F) := by
+    rw [hSymm, matVecMul_mul, matVecMul_mul, Matrix.mul_assoc,
+      Matrix.nonsing_inv_mul _ hUnit, Matrix.mul_one]
+  have hRight :
+      matVecMul (matSqrt S) G =
+        matVecMul (matSqrt S)⁻¹ (matVecMul S G) := by
+    obtain ⟨_, hSq⟩ := matSqrt_spec hS.posSemidef
+    have hMat : (matSqrt S)⁻¹ * S = matSqrt S := by
+      calc
+        (matSqrt S)⁻¹ * S =
+            (matSqrt S)⁻¹ * (matSqrt S * matSqrt S) :=
+          congrArg ((matSqrt S)⁻¹ * ·) hSq.symm
+        _ = ((matSqrt S)⁻¹ * matSqrt S) * matSqrt S :=
+          (Matrix.mul_assoc _ _ _).symm
+        _ = matSqrt S := by
+          rw [Matrix.nonsing_inv_mul _ hUnit, Matrix.one_mul]
+    calc
+      matVecMul (matSqrt S) G = matVecMul ((matSqrt S)⁻¹ * S) G := by rw [hMat]
+      _ = matVecMul (matSqrt S)⁻¹ (matVecMul S G) :=
+        (matVecMul_mul _ _ _).symm
+  calc
+    matVecMul ((matSqrt S)⁻¹ * A * matTranspose (matSqrt S)⁻¹)
+          (matVecMul (matSqrt S) F) - matVecMul (matSqrt S) G =
+        matVecMul (matSqrt S)⁻¹ (matVecMul A F) -
+          matVecMul (matSqrt S) G := by rw [hLeft]
+    _ = matVecMul (matSqrt S)⁻¹ (matVecMul A F) -
+          matVecMul (matSqrt S)⁻¹ (matVecMul S G) := by rw [← hRight]
+    _ = matVecMul (matSqrt S)⁻¹
+          (matVecMul A F - matVecMul S G) := by
+      funext i
+      simp only [Pi.sub_apply, matVecMul, mul_sub, Finset.sum_sub_distrib]
+
+/-- The preceding identity in the skew-centered convention of the
+homogenization theorem. -/
+theorem matSqrt_inv_skewCentered_flux_difference_eq {abar A : Mat d}
+    (hS : (symmPart abar).PosDef) (F G : Vec d) :
+    matVecMul
+          ((matSqrt (symmPart abar))⁻¹ * (A - skewPart abar) *
+            matTranspose (matSqrt (symmPart abar))⁻¹)
+          (matVecMul (matSqrt (symmPart abar)) F) -
+        matVecMul (matSqrt (symmPart abar)) G =
+      matVecMul (matSqrt (symmPart abar))⁻¹
+        (matVecMul (A - skewPart abar) F -
+          matVecMul (symmPart abar) G) :=
+  matSqrt_inv_centered_flux_difference_eq hS F G
+
+end
+
+end HighContrast
+end HCPolySupport