CorrectorLimitNode #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Provider: the corrector-limit lemma at the fresh shell #
ABK26, Lemma l.corrector.limit, specialized to the fresh shell.
Algsuperdiff/Section3/Provider/Corrector/CorrectorLimitFreshShell.lean proves
Step 4 modulo an exact Ω-level antisymmetric stream for the flux, and modulo
the sample-integrability of the two cube energies. This file removes both.
Removing the stream, the tolerance and the scale #
The stream the repository can build — exists_freshShellStream of
Algsuperdiff/Section3/Provider/Corrector/OmegaStreamAssembly.lean — represents
the flux only up to an L²(Ω) tolerance. Two parameters are eliminated:
- the tolerance
ε, byAlgsuperdiff/Section3/Provider/Corrector/SolenoidalApproximationEps.lean, where the gapE[|D − j|²]is shown to be independent of the cube and is chosen after the Young parameter; and - the localization scale
L, which is chosen after the stream and before the cube, exactly as in the exact-stream proof.
Removing the integrability hypotheses #
integrable_cubeAverage_dirichlet_energy and
integrable_cubeAverage_neumann_energy below show that the cube energy of
any family satisfying the weak formulation of e.corrector.limit.pde is
automatically integrable in the sample — no measurability of the family in
the sample is assumed. The mechanism is the variational characterization of the
two cube problems. Writing U = cu_K, F = f(· + ω) and ⟪·,·⟫ for the
L²(U) pairing, the Dirichlet gradient D satisfies
∫_U |D|² = sup { -2⟪F, v⟫ - ⟪v, v⟫ : v ∈ L²_{pot,0}(U) },
the supremum being attained at v = D because ⟪D + F, D⟫ = 0; the Neumann
gradient satisfies the same identity with L²_{pot}(U) in place of
L²_{pot,0}(U). Since L²(U; ℝᵈ) is second countable, the admissible class
has a countable dense subset and the supremum may be restricted to it. Each
member of the resulting countable family contributes a genuinely measurable
function of the sample — the competitor is a fixed field, so the sample
dependence enters only through the realization F, which is jointly measurable
by
Algsuperdiff.Section3.Provider.Corrector.stronglyMeasurable_uncurry_realize.
The energy is therefore a countable supremum of measurable functions, hence
measurable, and the a priori bound ∫_U |D|² ≤ ∫_U |F|² (the Hoelder display in
Step 2; it is NOT e.lower.bound.corrector.limit, which is the separate
lower-bound display) dominates it by an integrable function.
What the fresh-shell theorem takes #
Only the manuscript's own hypothesis "let w_D^{(K)}, w_N^{(K)} be the
solutions" of e.corrector.limit.pde: the two gradient families enter as
Dfam, Nfam carrying the weak formulations of that display, and nothing else.
Existence of the two cube solutions at every sample is unconditional — the
fresh-shell forcing has continuous realizations, and
Algsuperdiff/Section3/Provider/Diffusivity/Corrector/FreshShellExistence.lean
solves both cube problems for every continuous forcing — and their gradients are
unique.
The concrete-witness discipline #
CoarseGraining's IsSolenoidalZeroNormalTraceOn U g is orthogonality to
∇H¹(U) and carries no square integrability. The Neumann half below is
therefore routed through the concrete competitor family localStreamApprox
and its companion per-sample membership, never through an existential witness
of that predicate; see the module docstring of
SolenoidalApproximationEps.lean.
The deterministic comparison lemmas, in tested form #
Algsuperdiff/Section3/Provider/Corrector/CubeComparison.lean supplies the shared
tested comparison and integral identities. The remaining attainment and forcing
bounds below use only ∫_U (D + F) · v = 0, for both boundary conditions.
The admissible competitors as a subset of L²(U; ℝᵈ) #
The L²(U; ℝᵈ) image of the admissible class P. For the Dirichlet cube
problem P is Homogenization.IsPotentialZeroTraceOn U, for the Neumann cube
problem Homogenization.IsPotentialOn U. Only its separability is used, so no
submodule structure is needed.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The variational representation and its consequences #
The two cube energies #
The Dirichlet cube energy is automatically sample integrable.
Dfam is any family of vector fields satisfying, at almost every sample, the
weak formulation of the Dirichlet cube problem -Δ w = ∇·f in cu_K,
w ∈ H¹₀(cu_K) of ABK26: Dfam ω is a
zero-trace potential field and Dfam ω + f(· + ω) is solenoidal. Nothing is
assumed about the dependence of Dfam on the sample. Then the cube average of
|Dfam ω|² is integrable, so that the expectation
E[‖∇w_D^{(K)}‖²_{L²(cu_K)}] of the lemma is well defined.
The Neumann cube energy is automatically sample integrable.
Nfam is any family of vector fields satisfying, at almost every sample, the
weak formulation of the Neumann cube problem -Δ w = ∇·f in cu_K, n · (∇w + f) = 0 on ∂cu_K of ABK26: Nfam ω is a potential field and Nfam ω + f(· + ω) is solenoidal with vanishing normal trace. Nothing is assumed about the
dependence of Nfam on the sample. Then the cube average of |Nfam ω|² is
integrable, so that the expectation E[‖∇w_N^{(K)}‖²_{L²(cu_K)}] of the lemma
is well defined.
The corrector limit for a flux with approximate streams #
e.corrector.limit for a stationary flux possessing approximate
antisymmetric streams at every tolerance.
Let f be a stationary square-integrable forcing, let ∇w = p be the
whole-space stationary corrector gradient — the element of L²(Ω;ℝᵈ)
characterized by ∇w ∈ L²_pot(Ω) (hpmem) and f + ∇w ∈ L²_sol(Ω)
(hflux) — and let j = f + ∇w be the stationary flux (hjdef). Let
∇w_D^{(K)} = Dfam K and ∇w_N^{(K)} = Nfam K be the gradients of the two
solutions of e.corrector.limit.pde. Then
lim_K E[‖∇w_D^{(K)}‖²_{L²(cu_K)}] = lim_K E[‖∇w_N^{(K)}‖²_{L²(cu_K)}] = E[|∇w|²],
both limits existing.
hstream is the approximate representation hypothesis, in the exact shape
produced by exists_freshShellStream: for every tolerance η > 0 there is a
stationary square-integrable antisymmetric stream with smooth realizations whose
row divergence is the realization of a stationary square-integrable D with
E[|D − j|²] ≤ η. No exact stream is required, no integrability of a cube
energy is assumed, and neither the conclusion nor either one-sided bound is a
hypothesis.