Skip to content

WIP: Import Coarse-graining theory for elliptic equations #507

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Vilin97 wants to merge 62 commits into
base: main
Choose a base branch
from
Open

WIP: Import Coarse-graining theory for elliptic equations #507

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
62 commits
Select commit Hold shift + click to select a range
12d92d4
Import Coarse-graining theory for elliptic equations with source attr…
Vilin97 Sep 21, 2026
2a283bc
Port complete upstream content to current Mathlib and improve lint co…
Vilin97 Sep 21, 2026
a8e14fc
Port normalized Lp formulas while preserving arbitrary representative…
Vilin97 Sep 22, 2026
0a4a1c0
Port cutoff, convolution, and probability estimates to current Mathlib
Vilin97 Sep 22, 2026
8a806e1
Update localization and law transport for current measure APIs
Vilin97 Sep 22, 2026
ed53565
Port finite exponent fold transport and weak gradient closure
Vilin97 Sep 22, 2026
ab5f23f
Port Sobolev estimates while preserving integral seminorm contracts
Vilin97 Sep 22, 2026
ed3d44e
Preserve fractional integral identities and port convergence estimates
Vilin97 Sep 22, 2026
0169297
Preserve fractional integral norm laws across the Mathlib upgrade
Vilin97 Sep 22, 2026
f7520a9
Port Sobolev membership and smoothing measure arguments
Vilin97 Sep 22, 2026
43cb586
Update Sobolev approximation and completed dual norm bridges
Vilin97 Sep 22, 2026
deadb09
Update Poincare estimates and affine norm transport APIs
Vilin97 Sep 22, 2026
7e3e85f
Port Sobolev mollification and cube Poisson norm estimates
Vilin97 Sep 22, 2026
a56155b
Update weak equation transport and normalized Sobolev norm bridges
Vilin97 Sep 22, 2026
ca83766
Preserve unconditional reflection norms with measurability equivalences
Vilin97 Sep 22, 2026
6e59ba3
Preserve integral norm contracts and port mixed reflections
Vilin97 Sep 22, 2026
36b7586
Retain raw integral meaning of the cube Lp norm
Vilin97 Sep 22, 2026
78d00ae
Transport cube projection and overlap norms through integral seminorms
Vilin97 Sep 22, 2026
bf0de1e
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 22, 2026
2491831
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 23, 2026
f1d1682
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 23, 2026
a7f9659
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 24, 2026
2305358
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 24, 2026
73c0fd1
Restore project registration lost during automatic main merge
Vilin97 Sep 24, 2026
efedd2e
Port Poisson norm bridges and mapped probability instance
Vilin97 Sep 25, 2026
459546e
Merge remote-tracking branch 'origin/codex/import42-coarsegraining' i…
Vilin97 Sep 25, 2026
cda1745
Preserve raw norm congruence and transport across downstream bridges
Vilin97 Sep 25, 2026
2bc0a22
docs(CoarseGraining): state endpoint law and dimension assumptions
Vilin97 Sep 25, 2026
8e1210c
Merge current main preserving every project card
Vilin97 Sep 25, 2026
bfd3e02
Port coarse-graining module interfaces and raw norm bridges
Vilin97 Sep 25, 2026
2126cb1
Merge remote-tracking branch 'origin/codex/import42-coarsegraining' i…
Vilin97 Sep 25, 2026
18ae746
Bridge integral cube norms through measurable translations
Vilin97 Sep 25, 2026
7e2e4cb
Factor the two-exponent response localization proof
Vilin97 Sep 25, 2026
29c3f6a
Merge remote-tracking branch 'origin/codex/import42-coarsegraining' i…
Vilin97 Sep 25, 2026
ddb979d
Separate Caccioppoli scaling and descendant translation proofs
Vilin97 Sep 25, 2026
5ae0d8a
Isolate scalar bounds and shared canonical-average L2 facts
Vilin97 Sep 25, 2026
ae9d870
Factor canonical matrix positivity and forcing-tail root estimates
Vilin97 Sep 25, 2026
f335790
Separate coarse-graining scalar estimates and public basic modules
Vilin97 Sep 25, 2026
9c051ac
Share descendant geometry and stationary-law transport proofs
Vilin97 Sep 25, 2026
c5de9ca
Factor moment normalization and paired fluctuation estimates
Vilin97 Sep 25, 2026
6cbf6b2
Share finite-moment and low-scale fluctuation proof steps
Vilin97 Sep 25, 2026
bd9fc55
Separate excess regularity from low-scale expectation assembly
Vilin97 Sep 25, 2026
014bf81
Share positive-excess moment estimates and cutoff bounds
Vilin97 Sep 26, 2026
7bb44df
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
7d3f971
Merge main and preserve all YAML project registrations
Vilin97 Sep 26, 2026
8afd2be
Share multiplier derivative and Bennett integrability arguments
Vilin97 Sep 26, 2026
e619e7e
Merge remote-tracking branch 'origin/codex/import42-coarsegraining' i…
Vilin97 Sep 26, 2026
708ce1e
Separate matched positive-part convergence from gradient convergence
Vilin97 Sep 26, 2026
47086bd
Share cube cutoff geometry and isolate linear response estimates
Vilin97 Sep 26, 2026
ce8c707
Factor finite-exponent cube embedding convergence estimates
Vilin97 Sep 26, 2026
b2483bf
Restore public interfaces and explicit measurable norm bridges
Vilin97 Sep 26, 2026
a061b52
Reuse inferred cutoff product scalar comparisons
Vilin97 Sep 26, 2026
41136b9
Reuse component probe integrability in matrix averaging
Vilin97 Sep 26, 2026
ade930b
Compose annealed tail coefficient and decay bounds directly
Vilin97 Sep 26, 2026
3586777
Reuse Coarse tail parameters and repair module interfaces
Vilin97 Sep 26, 2026
72c6644
Preserve raw norm scaling and expose Poincare data interfaces
Vilin97 Sep 26, 2026
714ad44
Use existing exponent positivity certificates directly
Vilin97 Sep 26, 2026
dc98548
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 26, 2026
dd37265
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 26, 2026
b1547c6
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 26, 2026
b9d7519
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 26, 2026
b010378
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot] Sep 26, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1,640 changes: 1,640 additions & 0 deletions LeanPool.lean
View file
Open in desktop

Large diffs are not rendered by default.

1,615 changes: 1,615 additions & 0 deletions LeanPool/CoarseGraining.lean
View file
Open in desktop

Large diffs are not rendered by default.

183 changes: 183 additions & 0 deletions LeanPool/CoarseGraining/Homogenization.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,183 @@
/-
Copyright (c) 2026 Scott Armstrong, Tuomo Kuusi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Armstrong, Tuomo Kuusi
-/
module


public import LeanPool.CoarseGraining.Homogenization.Ambient.Basic
public import LeanPool.CoarseGraining.Homogenization.Ambient.HilbertFinite
public import LeanPool.CoarseGraining.Homogenization.Ambient.Euclidean
public import LeanPool.CoarseGraining.Homogenization.Ambient.CoefficientField
public import LeanPool.CoarseGraining.Homogenization.Geometry.Domain
public import LeanPool.CoarseGraining.Homogenization.Geometry.BoundedMeasurableDomain
public import LeanPool.CoarseGraining.Homogenization.Geometry.TriadicCube
public import LeanPool.CoarseGraining.Homogenization.Geometry.TriadicCubeTranslation
public import LeanPool.CoarseGraining.Homogenization.Geometry.TriadicPartition
public import LeanPool.CoarseGraining.Homogenization.Geometry.BoundaryLayer
public import LeanPool.CoarseGraining.Homogenization.Geometry.CubeMeasure
public import LeanPool.CoarseGraining.Homogenization.Geometry.OriginCubeMeasureBridge
public import LeanPool.CoarseGraining.Homogenization.Geometry.OriginCubeBoundaryPush
public import LeanPool.CoarseGraining.Homogenization.Geometry.ConvexDomain
public import LeanPool.CoarseGraining.Homogenization.Geometry.CubeColoring
public import LeanPool.CoarseGraining.Homogenization.Multiscale.CubeAverage
public import LeanPool.CoarseGraining.Homogenization.Multiscale.FiniteAverage
public import LeanPool.CoarseGraining.Homogenization.Multiscale.Projection
public import LeanPool.CoarseGraining.Homogenization.Multiscale.NormalizedNorms
public import LeanPool.CoarseGraining.Homogenization.Multiscale.ProjectionLp
public import LeanPool.CoarseGraining.Homogenization.Besov.Basic
public import LeanPool.CoarseGraining.Homogenization.Besov.Positive
public import LeanPool.CoarseGraining.Homogenization.Besov.PositiveOverlapBridge
public import LeanPool.CoarseGraining.Homogenization.Besov.Negative
public import LeanPool.CoarseGraining.Homogenization.Besov.Duality
public import LeanPool.CoarseGraining.Homogenization.Besov.ProjectionCharacterization
public import LeanPool.CoarseGraining.Homogenization.Besov.Poincare.HarmonicGradient
public import LeanPool.CoarseGraining.Homogenization.Sobolev.L2Ambient
public import LeanPool.CoarseGraining.Homogenization.Sobolev.H1
public import LeanPool.CoarseGraining.Homogenization.Sobolev.W1p
public import LeanPool.CoarseGraining.Homogenization.Sobolev.H1.OriginCubeSymmetry
public import LeanPool.CoarseGraining.Homogenization.Sobolev.PotentialSolenoidal
public import LeanPool.CoarseGraining.Homogenization.Sobolev.PotentialSolenoidalCubeBridge
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.Hodge
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.MeanZero
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.CoerciveH1
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.CoerciveSmooth
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.CoerciveH10
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.CoerciveMeanZero
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.PoincareMeanZero
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.PoincareW1p
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.PoincareZeroTrace
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.H10Graph
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.AffineAverage
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.QuantitativeCutoff
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.AxisCube
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.Cutoff.OpenSet
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.Cutoff.Box
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Truncation.MatchedTrace
public import LeanPool.CoarseGraining.Homogenization.Sobolev.CubeEmbedding
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Foundations.CubeCalderonZygmund
public import LeanPool.CoarseGraining.Homogenization.Sobolev.MatchedPair
public import LeanPool.CoarseGraining.Homogenization.Sobolev.PotentialSolenoidalOriginCubeSymmetry
public import LeanPool.CoarseGraining.Homogenization.Sobolev.PotentialSolenoidalL2
public import LeanPool.CoarseGraining.Homogenization.Sobolev.PotentialSolenoidalL2Realization
public import LeanPool.CoarseGraining.Homogenization.PDE.Harmonic
public import LeanPool.CoarseGraining.Homogenization.PDE.HarmonicTranslation
public import LeanPool.CoarseGraining.Homogenization.PDE.HarmonicCube
public import LeanPool.CoarseGraining.Homogenization.PDE.HarmonicHilbert
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.BlockFormalism
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.HilbertMinimization
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.HilbertMinimizationMeasurability
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.MuWellPosedness
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.Definitions
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.MuQuadratic
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.MuOperator
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.MuRecovery
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.ResponseIdentities.ConvexAverageFormulas
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.MuRecoveryBlockResponse
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.OriginCubeEllipticRecovery
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.Symmetric
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.OriginCubeOpenBridge
public import LeanPool.CoarseGraining.Homogenization.Deterministic.MultiscaleQuantities
public import LeanPool.CoarseGraining.Homogenization.Deterministic.WeakFluxRHS
public import LeanPool.CoarseGraining.Homogenization.Deterministic.WeakNormInterfaces.HodgeZero
public import LeanPool.CoarseGraining.Homogenization.Deterministic.HomogenizationBlackBoxes
public import LeanPool.CoarseGraining.Homogenization.Probability.RandomField
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.Sigma
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.EllipticSet
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.Endomorphisms
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.Restriction
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.RestrictionBridge
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.Laws
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.Differentiation
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.SliceMeasurability
public import LeanPool.CoarseGraining.Homogenization.Probability.RegCoeffField.EllipticSupport
public import LeanPool.CoarseGraining.Homogenization.Probability.Source.Coarse.Semantics
public import LeanPool.CoarseGraining.Homogenization.Probability.SeparableHilbertMeasurability
public import LeanPool.CoarseGraining.Homogenization.Probability.LocalEllipticitySlices
public import LeanPool.CoarseGraining.Homogenization.Probability.RandomFieldMeasurability
public import LeanPool.CoarseGraining.Homogenization.Probability.RandomCoeffField
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.WeakOrlicz
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.PsiCalculus
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.Triangle
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.PsiConcentration
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.IndependentCopy
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.Rosenthal
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.GammaSigma
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.GammaSigmaExpRegime
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.GammaSigmaConcentration
public import LeanPool.CoarseGraining.Homogenization.Probability.IndependentSums.PsiSigma
public import LeanPool.CoarseGraining.Homogenization.Probability.RescaledLaw
public import LeanPool.CoarseGraining.Homogenization.Probability.Scalarization
public import LeanPool.CoarseGraining.Homogenization.Probability.OriginCubeSymmetry
public import LeanPool.CoarseGraining.Homogenization.Probability.EfronStein
public import LeanPool.CoarseGraining.Homogenization.Probability.EfronStein.Transfer

public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.ThetaEllipticity
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.SharpBlockBounds
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.QuadraticStability
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.CubeMinimizer
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.CoarseBounds


public import LeanPool.CoarseGraining.Homogenization.Book.Ch01
public import LeanPool.CoarseGraining.Homogenization.Book.Ch01.Theorems.MeanSquareDeviation
public import LeanPool.CoarseGraining.Homogenization.Book.Ch02
public import LeanPool.CoarseGraining.Homogenization.Book.Ch03
public import LeanPool.CoarseGraining.Homogenization.Book.Ch04
public import LeanPool.CoarseGraining.Homogenization.Book.Ch04.Theorems.DilationResponse
public import LeanPool.CoarseGraining.Homogenization.Book.Ch05

public import LeanPool.CoarseGraining.Homogenization.Besov.Poincare
public import LeanPool.CoarseGraining.Homogenization.Book
public import LeanPool.CoarseGraining.Homogenization.Book.Ch01.Theorems.FractionalSobolevVsBesov
public import LeanPool.CoarseGraining.Homogenization.Book.Ch02.Interfaces
public import LeanPool.CoarseGraining.Homogenization.Book.Ch03.Theorems.SobolevPublic
public import LeanPool.CoarseGraining.Homogenization.Book.Ch04.AnnealedObjects
public import LeanPool.CoarseGraining.Homogenization.Book.Ch05.Theorems.Section54.VarianceBoundGoodScale.Assembly
public import LeanPool.CoarseGraining.Homogenization.Book.Ch05.Theorems.Section57.UniformEllipticityBridge
public import LeanPool.CoarseGraining.Homogenization.Book.MainResults
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.AdjointSymmetry
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.AdjointSymmetry.EllipticWrappers
public import LeanPool.CoarseGraining.Homogenization.CoarseGraining.ResponseIdentities
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarseCaccioppoli
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.HarmonicFinal
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarseCaccioppoliEnergyBridge
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarseCaccioppoliSingleCubeToRaw
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarsePoincare
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarsePoincareRHS
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarsePoincareRHS.Compatibility
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarsePoincareRHS.Energy
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarsePoincareRHS.FinalTheorems
public import LeanPool.CoarseGraining.Homogenization.Deterministic.CoarsePoincareRHSLocalRecurrence
public import LeanPool.CoarseGraining.Homogenization.Examples.Periodic.DiracBridge
public import LeanPool.CoarseGraining.Homogenization.Examples.Periodic.MField
public import LeanPool.CoarseGraining.Homogenization.Examples.Periodic.PeriodicConcreteComparison
public import LeanPool.CoarseGraining.Homogenization.Examples.Periodic.PeriodicGeneralComparison
public import LeanPool.CoarseGraining.Homogenization.Examples.Periodic.PeriodicSmoothComparison
public import LeanPool.CoarseGraining.Homogenization.Examples.RandomCheckerboard.Basic
public import LeanPool.CoarseGraining.Homogenization.Examples.RandomCheckerboard.CarrierLaw
public import LeanPool.CoarseGraining.Homogenization.Examples.RandomCheckerboard.SourceLaw
public import LeanPool.CoarseGraining.Homogenization.Examples.RandomCheckerboard.AKLLaw
public import LeanPool.CoarseGraining.Homogenization.Internal
public import LeanPool.CoarseGraining.Homogenization.Internal.Ch02
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.AssemblyPieces
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.BesovLeGagliardo
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.ClassicalDualComparison
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.CongruenceAE
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.Constants
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.Definitions
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.DefinitionsAPI
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.ENNRealBridge
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.GagliardoLeBesov
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.JensenStep
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.OverlapCount
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.OverlapIntegral
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.PairCapture
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.ShellGeometry
public import LeanPool.CoarseGraining.Homogenization.Sobolev.Fractional.TailSummation

/-! # Homogenization -/

@[expose] public section
20 changes: 20 additions & 0 deletions LeanPool/CoarseGraining/Homogenization/Ambient.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
/-
Copyright (c) 2026 Scott Armstrong, Tuomo Kuusi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Armstrong, Tuomo Kuusi
-/
module


public import LeanPool.CoarseGraining.Homogenization.Ambient.Basic
public import LeanPool.CoarseGraining.Homogenization.Ambient.BlockMatrix
public import LeanPool.CoarseGraining.Homogenization.Ambient.CoefficientField
public import LeanPool.CoarseGraining.Homogenization.Ambient.CoefficientFieldHilbert
public import LeanPool.CoarseGraining.Homogenization.Ambient.Euclidean
public import LeanPool.CoarseGraining.Homogenization.Ambient.HilbertFinite
public import LeanPool.CoarseGraining.Homogenization.Ambient.MatrixOrderBridge
public import LeanPool.CoarseGraining.Homogenization.Ambient.ScalarMatrix

/-! Supporting modules for Coarse-graining theory for elliptic equations. -/

@[expose] public section
Loading
Loading