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

Open

Vilin97 wants to merge 200 commits into

mainfrom

codex/import42-coarsegraining

Commits on Sep 21, 2026

Import Coarse-graining theory for elliptic equations with source attribution and complete production scope
Vilin97
committed
12d92d4
Port complete upstream content to current Mathlib and improve lint compliance
Vilin97
committed
2a283bc

Commits on Sep 22, 2026

Port normalized Lp formulas while preserving arbitrary representative semantics
Vilin97
committed
a8e14fc
Port cutoff, convolution, and probability estimates to current Mathlib
Vilin97
committed
0a4a1c0
Update localization and law transport for current measure APIs
Vilin97
committed
8a806e1
Port finite exponent fold transport and weak gradient closure
Vilin97
committed
ed53565
Port Sobolev estimates while preserving integral seminorm contracts
Vilin97
committed
ab5f23f
Preserve fractional integral identities and port convergence estimates
Vilin97
committed
ed3d44e
Preserve fractional integral norm laws across the Mathlib upgrade
Vilin97
committed
0169297
Port Sobolev membership and smoothing measure arguments
Vilin97
committed
f7520a9
Update Sobolev approximation and completed dual norm bridges
Vilin97
committed
43cb586
Update Poincare estimates and affine norm transport APIs
Vilin97
committed
deadb09
Port Sobolev mollification and cube Poisson norm estimates
Vilin97
committed
7e3e85f
Update weak equation transport and normalized Sobolev norm bridges
Vilin97
committed
a56155b
Preserve unconditional reflection norms with measurability equivalences
Vilin97
committed
ca83766
Preserve integral norm contracts and port mixed reflections
Vilin97
committed
6e59ba3
Retain raw integral meaning of the cube Lp norm
Vilin97
committed
36b7586
Transport cube projection and overlap norms through integral seminorms
Vilin97
committed
78d00ae
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
bf0de1e

Commits on Sep 23, 2026

Commits on Sep 24, 2026

Commits on Sep 25, 2026

Commits on Sep 26, 2026

Commits on Sep 27, 2026

Commits on Sep 28, 2026

Commits on Sep 29, 2026

Commits on Sep 30, 2026

Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
0487b74

Commits on Oct 1, 2026

Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
7a23ac9
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
62d754e
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
b68f2e7
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
6c8e26b
Update CoarseGraining imports for Mathlib 4.35
Vilin97
committed
e7ebad3
Merge project-root index migration for CoarseGraining
Vilin97
committed
2ca36fd
Shorten long CoarseGraining declaration names
Vilin97
committed
60f72a4
Shorten CoarseGraining declaration names in source batch three
Vilin97
committed
5614f8c
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
0885a14
Shorten CoarseGraining declarations and repair projections
Vilin97
committed
028378e
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
c444447
Use current measure theory APIs in CoarseGraining
Vilin97
committed
361c83c

Commits on Oct 2, 2026

Reflow Rosenthal endpoint estimates
Vilin97
committed
e4e9a39
Remove redundant CoarseGraining change tactics
Vilin97
committed
7e41691
Replace deprecated CoarseGraining measure and order lemmas
Vilin97
committed
440b58e
Wrap Ch04 canonical measurability expressions
Vilin97
committed
612cc33
Remove blank lines within CoarseGraining commands
Vilin97
committed
3fc6bd9
Shorten corrected-flux constant references in local bridge
Vilin97
committed
00f087b
Wrap MuRecovery correction-space energy expressions
Vilin97
committed
fc67ff4
Wrap Ch04 carrier minimizer expressions
Vilin97
committed
35fc111
Use explicit simplification in Ch04 expectations
Vilin97
committed
9d8b8cb
Close split OriginCube proof parentheses
Vilin97
committed
597cc08
Wrap bad maximal P1 expressions
Vilin97
committed
42cc95c
Shorten bad maximal P1 references and theorem name
Vilin97
committed
c669dd2
Resolve flexible simp warnings in fluctuation integrability
Vilin97
committed
97f81af
Tighten tactic bullet formatting in coarse graining
Vilin97
committed
c03fa18
Wrap coupled representation proof lines
Vilin97
committed
b8839f5
Wrap repeated Hessian Besov depth expressions
Vilin97
committed
e5a4b68
Wrap phase-averaging proof expressions
Vilin97
committed
f0634dc
Wrap high contrast variance and level-energy proofs
Vilin97
committed
b1a21b1
Wrap Euclidean fractional localization bounds
Vilin97
committed
9e70702
Wrap Efron Stein finite-product arguments
Vilin97
committed
7dce3b6
Wrap origin-cube Sobolev bridge expressions
Vilin97
committed
34468de
Close coarse graining sections and namespaces
Vilin97
committed
ebe60a5
Remove unused simplifier arguments in coarse graining
Vilin97
committed
3578e1b
Wrap Sobolev coercivity and smoothing proofs
Vilin97
committed
cacc99b
Shorten dual-test fluctuation theorem names
Vilin97
committed
131d17f
Wrap long Besov pairing expressions
Vilin97
committed
4dd95f5
Wrap Sobolev extension and submodule expressions
Vilin97
committed
5674543
Shorten recovered pair names and wrap response expressions
Vilin97
committed
657de3b
Use source hypotheses directly in reflection strip proofs
Vilin97
committed
f790df4
State reflection-neighbor coordinate bounds explicitly
Vilin97
committed
66dad3c
Wrap multiscale coefficient bounds
Vilin97
committed
049568c
Wrap multiscale ellipticity and descendant bounds
Vilin97
committed
67fc41d
Wrap coarse graining foundation declarations and proofs
Vilin97
committed
eaa4a1f
Wrap block response, response formula, and variance lines
Vilin97
committed
c8610a9
Make wrap around simplification steps explicit
Vilin97
committed
a356653
Make matrix and response simplifications explicit
Vilin97
committed
cb4035c
Make block Loewner integration simplifications explicit
Vilin97
committed
e14f050
Wrap Chapter 5 section 52 and 53 expressions
Vilin97
committed
68adc4d
Use explicit simplification in normalized block trace proofs
Vilin97
committed
e16253c
Make probability and projection simplifications explicit
Vilin97
committed
eb4be96
Use explicit moment simplification in Rosenthal bounds
Vilin97
committed
458ffb6
Fix scoped Ch05 simplification warnings
Vilin97
committed
1e07221
Wrap long CoarseGraining theorem declarations
Vilin97
committed
43abd8c
Wrap long CoarseGraining theorem declarations in eight modules
Vilin97
committed
458dcf5
Wrap long CoarseGraining theorem declarations in further modules
Vilin97
committed
2aa1c7f
Make CoarseGraining cube equality simplifications explicit
Vilin97
committed
b46467f
Wrap CoarseGraining Book theorem declarations
Vilin97
committed
a7707a7
Make projected Besov norm simplification explicit
Vilin97
committed
91bd9e6
Merge remote-tracking branch 'origin/codex/import42-coarsegraining' into codex/import42-coarsegraining
Vilin97
committed
d4ddd97
Merge remote-tracking branch 'origin/main' into codex/import42-coarsegraining
Vilin97
committed
b41b4be
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
530d886
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
576195e
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
41c2099
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
3b6d694
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
0b11056
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
c925596
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
5fb8c12
share paired-square normalization and measurability proofs
Vilin97
committed
bb56725
Merge remote-tracking branch 'origin/main' into HEAD
Vilin97
committed
db4cf5a
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
10de623
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
05f2236
Merge remote-tracking branch 'origin/main' into pr-507
github-actions[bot]
committed
fcb0e6e

Commits on Oct 3, 2026

Commits on Oct 4, 2026

Commits on Oct 5, 2026

Commits on Oct 6, 2026