CaccioppoliInteriorEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
e.energy.bound.interior at the parent slot #
This module assembles ABK26's interior coarse-grained Caccioppoli energy
estimate (e.energy.bound.interior) at the parent slot of the frozen §4.3
anchor, in the translated frame of resolution A4:
⨍_{□_{n+2} ∩ (w+□_n)} ∇u · ã_{L,n+2} ∇u · 1_𝒢
≤ C(d) ( σ_{n+2} 3^{-2(n+2)} ‖u - (u)_{□_{n+2}}‖²_{L²(□_{n+2})}
+ s^{-8} σ_{n+2}^{-1} [g]²_{B^s(□_{n+2})} ) ,
almost surely on the harmonic anchor's own good event
𝒢(n+2, z; s/8, 1/2), for every L ≥ n+2, every window centre w, and every
forced H¹(□_{n+2}) solution of -∇·ã_{L,n+2}∇u = ∇·g.
What each input supplies #
- the energy inequality: CoarseGraining's
coarseCaccioppoliRHSTheory, specialized to the interior regime and mean-subtracted inCaccioppoliInteriorDatum.lean; - the geometry:
CaccioppoliInteriorGeometry.lean(the corollary that identifies the Caccioppoli core with the translated child cubew + □_n).
What this module does NOT do (disclosed frontier) #
The forced equation on the parent cube, at the flux-corrected family and at the
translated sample, is an input. Producing it from the frozen theorem's
Dirichlet problem on □_m still needs, and this module does not contain:
- the restriction of the
□_mequation to the parent window (the interior gate(z+□_{n+2}) ⊆ □_m— proved inCaccioppoliInteriorGeometry.lean— plusH¹₀extension by zero, which CoarseGraining has for arbitrary open supersets); - the A4 translation transport of
H¹, of the coefficient field and of the Besov seminorm from the geometric windowz + □_{n+2}to the origin cube.
Likewise the passage from this estimate to the frozen theorem's own display
needs the ν^{1/2}‖∇u‖_{L²} ↔ ⨍ ∇u·ã∇u identification and a
Gagliardo-versus-Besov comparison (the anchor writes normalizedGagliardo,
CoarseGraining's Caccioppoli carries the block-average Besov seminorm).
1. The display object #
The right-hand side of e.energy.bound.interior, squared, at the parent
window. The mean-subtracted parent L² square plus the forcing seminorm
square, at the honest envelope s^{-8}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The same display at the printed envelope s^{-11} (the square of the
printed s^{-11/2}).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The honest envelope is stronger than the printed one on the anchor's
s-range: s^{-8} ≤ s^{-11} for 0 < s ≤ 1.
2. The arithmetic stitch #
3. The energy estimate on the good event #
e.energy.bound.interior at the parent slot, in the translated frame.
Almost surely on the harmonic anchor's good event 𝒢(n+2, z; s/8, 1/2), for
every L ≥ n+2, every window centre w whose Dirichlet patch w + □_{n+1}
sits inside □_{n+2} (the interior regime), and every H¹(□_{n+2}) solution of
-∇·ã_{L,n+2}∇u = ∇·g with g ∈ H^s(□_{n+2}),
⨍_{□_{n+2} ∩ (w+□_n)} ∇u · ã_{L,n+2} ∇u ≤ Cout · interiorEnergyRHS M n s u g .
The two constants are separate: C is the annular anchor's regime constant,
Cout the output constant.
4. The frozen theorem's own geometry, at the printed envelope #
e.energy.bound.interior read at the frozen theorem's geometry binder.
Under the anchor's own binder (x+□_n) ⊆ (z+□_{n+1}) ∩ □_m, the Caccioppoli core
of the translated frame is the translated child cube (x-z) + □_n, and the
Dirichlet patch inclusion is automatic. The right-hand side is stated at the
printed envelope s^{-11} (the square of s^{-11/2}), which the honest
s^{-8} dominates on the anchor's s-range:
⨍_{(x-z)+□_n} ∇u · ã_{L,n+2} ∇u · 1_𝒢
≤ C(d) ( σ_{n+2} 3^{-2(n+2)} ‖u - (u)_{□_{n+2}}‖²_{L²(□_{n+2})}
+ s^{-11} σ_{n+2}^{-1} [g]²_{B^s(□_{n+2})} ) .
The frontier-empty gate of the anchor's second conjunct is not consumed here:
it is what the caller needs in order to restrict the □_m equation to the parent
(see CaccioppoliInteriorGeometry.lean and the module docstring).