CubeComparison #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the per-realization comparison layer of the corrector-limit proof #
ABK26, Lemma l.corrector.limit, works at each fixed realization with the two
cube problems
-Δ w_D^{(K)} = ∇ · f in cu_K, w_D^{(K)} = 0 on ∂cu_K, and
-Δ w_N^{(K)} = ∇ · f in cu_K, n · (∇ w_N^{(K)} + f) = 0 on ∂cu_K.
IsPotentialZeroTraceOn U Dtogether withIsSolenoidalOn U (D + f), andIsPotentialOn U Ntogether withIsSolenoidalZeroNormalTraceOn U (N + f),
which are literal transcriptions of e.corrector.limit.pde: the first pair says
w_D^{(K)} ∈ H¹₀(cu_K) and ⨍ (∇w_D^{(K)} + f) · ∇φ = 0 for every φ ∈ H¹₀(cu_K), the second says w_N^{(K)} ∈ H¹(cu_K) and the same identity for
every φ ∈ H¹(cu_K), the natural boundary condition.
This file proves, at a single realization and on an arbitrary domain, the two purely deterministic facts the proof extracts from those formulations:
e.ordering.corrector.limit, the Step-1 ordering‖∇w_D^{(K)}‖²_{L²} ≤ ‖∇w_N^{(K)}‖²_{L²}; and- the Step-2 comparison against an admissible zero-trace competitor, in the
sharp form
‖D‖² ≥ -2⟪f, v⟫ - ‖v‖², which is the statement thatDminimizesE(v) = ½‖v‖² + ⟪f, v⟫over the zero-trace potential fields.
Both are unconditional: no approximation lemma, no stationarity, and no
probability enters here. The abstract Hilbert-space versions of the same two
facts are in Algsuperdiff/Section3/Provider/Corrector/VariationalEnergy.lean;
this file is their concrete counterpart on the CoarseGraining Sobolev carriers,
where the admissible classes are IsPotentialZeroTraceOn and IsPotentialOn
rather than abstract submodules.
Pointwise algebra of the Euclidean dot product #
The polarization expansion |a - b|² = |a|² - 2 a · b + |b|² for the
Euclidean dot product of the project's vector carrier Vec d.
The polarization expansion |a + b|² = |a|² + 2 a · b + |b|².
The Euclidean dot product of a vector with itself is nonnegative.
The squared-distance polarization identity integrated over any domain.
Testing the weak formulations #
Testing a solenoidal field against a zero-trace potential competitor. With
g = ∇w_D^{(K)} + f this is the first display of
e.testing.by.vKL.corrector.limit.
Testing a solenoidal field with vanishing normal trace against an arbitrary
potential competitor. With g = ∇w_N^{(K)} + f this is the Neumann natural
boundary condition used in Step 3 of ABK26.
Every zero-trace potential field is a potential field: H¹₀(U) ⊆ H¹(U).
This is the inclusion behind e.ordering.corrector.limit.
Splitting the tested flux into its two square-integrable halves.
Completing the square bounds the energy from a single tested flux identity.
The Step-2 comparison #
Step 2 of l.corrector.limit at a fixed realization.
If D is the gradient of the H¹₀(U) solution of -Δw = ∇·F, i.e. D is a
zero-trace potential field with D + F solenoidal, then for every admissible
zero-trace competitor v
-2 ∫_U F · v - ∫_U |v|² ≤ ∫_U |D|².
Equivalently D minimizes E(v) = ½∫|v|² + ∫F·v over the zero-trace potential
fields, which is the variational characterization asserted in Step 1 and used in
Step 2 with v = ∇v_{K,L}.
Only the weak formulation and square integrability are used; no boundary regularity, no approximation lemma and no probability.
The flux rewriting of the Step-2 comparison. Completing the square turns
-2 ∫ F · v - ∫ |v|² into ∫ |F|² - ∫ |v + F|², which is the form the
corrector-limit proof uses: the competitor enters only through the flux
v + F, whose stationary limit is ∇w + f.
The Step-2 comparison in flux form. For every admissible zero-trace
competitor v,
∫_U |F|² - ∫_U |v + F|² ≤ ∫_U |D|².
This is the shape consumed in the infinite-volume limit: the left-hand side
converges to E[|f|²] - E[|f + ∇w|²] = E[|∇w|²] when v approximates ∇w.
The Step-1 ordering #
e.ordering.corrector.limit at a fixed realization: the Dirichlet
gradient carries no more energy than the Neumann gradient,
∫_U |∇w_D|² ≤ ∫_U |∇w_N|².
D is the gradient of the H¹₀(U) solution and N the gradient of the
H¹(U) solution of the same equation -Δw = ∇·F, the Neumann natural boundary
condition being IsSolenoidalZeroNormalTraceOn U (N + F). The proof is the
paper's: H¹₀(U) ⊆ H¹(U), so the Neumann energy is the smaller of the two, and
the energy identity converts that into the displayed ordering of the gradient
norms.