HomStepFourEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Theorem B, §4.5, Step 4: the introduction's energy display #
The assembly #
|⨍ ν|∇u|² - ⨍ σ_m|∇v|²|
= |⨍ (a_L∇u - σ_m∇v)·∇v + σ_m ⨍ (∇u-∇v)·∇v| (§3)
≤ (W_flux + σ_m W_grad) · ‖∇v‖_{W^{s,∞}} (§4)
≤ (3^{ms}σ_m C E D + σ_m 3^{ms} C E D) · C_sch 3^{-ms} D
= 2 C C_sch E · σ_m D² = 2 C C_sch E · bracket², (§5)
the last step being the EXACT identity σ D² = bracket²
(sigma_mul_sq_dataBracket), where D is the un-square-rooted data bracket of
the introduction's homogenization estimate and bracket the square-rooted one
of the introduction's energy display. No inequality is spent there: the two
printed brackets differ by exactly one factor √σ_m.
The three inputs, and which of them is a hypothesis #
- the flux weak bound and the gradient weak bound. The
manuscript's own justification reads BOTH
off ONE application of the general coarse-graining proposition, whose printed conclusion carries
the two halves in a single sum on the left. They
are therefore ONE transcribed source hypothesis, not two, and they arrive at
the duality carrier of
HomStepFourPairing. - the Schauder bound on
‖∇v‖_{W^{s,∞}(□_m)}. This is The manuscript's Schauder step: "By Schauder estimates for the Poisson equation in a cube (by odd reflection)" is asserted with no citation and no labelled in-paper result, and bullet 2 records it as deferred to reflection folklore. Nothing in the manuscript, in this repository, or inCoarseGrainingproves it (surveyed: theProvider/ExcessDecay/OneStepSchauder*chain is the ZERO-forcing interior/odd-reflection estimate for the harmonic competitor on the §4.3 replacement window; there is no-σΔv = ∇·ggradient-Hölder estimate anywhere, and an earlier rebuild carried the same bound as an ASSUMED field). It therefore enters here as a NAMED TRANSCRIBED hypothesishSch, in exactly the printed shape, and is disclosed as a THIRD conditional of clause (C4) beyond{hC, hCG}.
1. Linearity of the volume average #
2. The ν-drop at the volume average #
⨍ ν|∇u|² = ⨍ ∇u·a∇u (a correction to the printed statement), pointwise and hence at
the average. ν is not divided by anything and no ellipticity is used.
The comparator's energy density at the scalar field σ Id.
3. The energy split #
The Step-4 energy split.
The pointwise identity of HomStepFourIdentity averaged, with the testing
identity substituted into the second summand:
⨍ ν|∇u|² - ⨍ σ|∇v|²
= ⨍ (a_L∇u - σ∇v)·∇v + σ ⨍ (∇u - ∇v)·∇v.
Both summands are cubePairings against the SAME test field ∇v, which is
what the two duality bounds consume. The three integrability hypotheses are
the manuscript's own u, v ∈ H¹(□_m) in force; they are stated rather than
smuggled.
4. The duality step #
The two pairings, applied. From the split and the two duality levels,
the energy difference is bounded by (W_flux + σ W_grad) times the test gauge
of ∇v.
5. The bracket arithmetic σ D² = bracket² #
The un-square-rooted data bracket of the introduction's homogenization estimate.
Equations
Instances For
The square-rooted data bracket of the introduction's energy display.
Equations
Instances For
The exact relation between the two printed brackets: √σ · D = bracket.
No inequality is spent: the introduction's energy display bracket is the
the introduction's homogenization estimate bracket multiplied by √σ_m.
σ D² = bracket², the form the assembly consumes.
6. The §4.5 display #
the introduction's energy display from the three §4.5 inputs.
The weak flux bound at level 3^{ms} σ (C E D), the weak gradient bound at
level 3^{ms} (C E D) — the two halves of the ONE coarse-graining application
— and the Schauder gauge C_sch 3^{-ms} D (the Schauder gap) compose to
|⨍ ν|∇u|² - ⨍ σ|∇v|²| ≤ 2 C C_sch E · σ D² = 2 C C_sch E · bracket².
Every constant is explicit; nothing is absorbed silently. The residual 2 C C_sch is exactly what's witness rescaling (ethmB_const_smul_moment)
transports through the moment bound.