HomStepTwoEnergy #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Theorem B, §4.5, Step 2a: the energy-from-data display #
The target (Theorem B, Step 2: the energy from data) #
ν^{1/2} ‖∇u‖_{L²(□_m)}
≤ C ( 1 + 𝓔_{1/4,∞,2}(□_m; ã_{L,m}, σ_m) ) ( σ_m^{-1/2} 3^{m/2} + σ_m^{1/2} 3^{m/2} )
proved, per the node's own EDGEs, from the coarse-graining right-hand side
and the display bounding the Λ's by the 𝓔's.
What is proved here, exactly #
The two named inputs, composed on the carriers:
- the coarse-graining right-hand side =
CoarseGraining'sCh03.energyConsequencesRHSTheory(Dirichlet half), entered through the carrier mapdirichletForcedCubeSolutionOfIsDirichlet SolutionOn(obstruction 2) and read on the left through theν-drop (obstruction 1); - the display bounding the
Λ's by the𝓔's =CoarseGraining'sCh02.max_weightedEllipticity_finite_two_le_card_mul_homogenizationError_sq_add_oneat the constant2d, transported byExcessDecay.max_ellipticityRatio_le_ homogenizationError.
The output (exists_sqrt_nu_mul_gradL2_le) is
ν^{1/2} ‖∇u‖_{L²(□_m)}
≤ C(d) t^{-3/2} · σ_m^{-1/2} √(2d) ( 1 + 𝓔_{t/2}(□_m; ã_{L,m}, σ_m) ) · B_g
+ C(d) t^{-1/2} · σ_m^{ 1/2} √(2d) ( 1 + 𝓔_{t} (□_m; ã_{L,m}, σ_m) ) · B_h
with B_g, B_h CoarseGraining's own note-normalized Besov data quantities
at index t (√(2d) is the display bounding the Λ's by the 𝓔's's own
dimensional loss, kept visible).
The three deviations from the printed display #
Each is visible in the statement; none is absorbed.
- TWO error indices, not one.
CoarseGraining's coarse-graining right-hand side placesλat the indext/2andΛat the indext(this is confirmed here in the definition ofCh03.dirichletEnergyWithRHSRHS). the display bounding theΛ's by the𝓔's is therefore instantiated TWICE, att/2and att, and the display carries𝓔_{t/2}and𝓔_tseparately. Collapsing them to the printed single𝓔_{1/4}needs an index-monotonicity of𝓔_{·,∞,2}that is NOT available:Ch02.geometricWeightnormalizes the scale weights to a probability distribution, sos ↦ 𝓔_{s,∞,2}is a weighted average whose monotonicity depends on the response sequence. The printed choice1/4moreover forcest = 1/2, at which the DATA leg is infinite forC^{0,1/2}data (correction ). RECORDED AS A SOURCE FINDING; the two-index display is the honest one and is what Step 3 can consume. - The
t-powers stay displayed:t^{-3/2}andt^{-1/2}areCoarseGraining's own prefactors of the coarse-graining right-hand side. At the §4.5 valuet = s = |log γ|⁻¹they are|log γ|^{3/2}and|log γ|^{1/2}, NOT constants; the source absorbs them intoCsilently and the node's ownNOTElicenses the absorption only because it is spent once. Nothing is absorbed here. - The data legs are
CoarseGraining's Besov quantities, not3^{m/2}. The passageB_g, B_h ≤ C 3^{m/2}is the data embedding, given in theH^s/Gagliardo carrier (HomBridgeDataEmbedding.three_rpow_mul_normalizedGagliardo_originCube_le_ pinned), butCoarseGraining's coarse-graining right-hand side states its data legs in the DYADIC-descendantcubeBesovcarrier. The Gagliardo →cubeBesovbridge exists (Provider.ExcessDecay.scaleNormalizedPositiveBesovVectorSeminormTwo_le_ gagliardo); its two side conditions —MemLp g 2andGagliardo.MemWsp Q t 2 gfrom a Hölder bound — do NOT exist and are the exact residue (they are the two Gagliardo-side atoms of the Step-2b family). SinceForceBesovRegularityis ALSO a hypothesis of the coarse-graining right-hand side itself, the two residues are the same two atoms; nothing else is missing.
1. Two rpow spellings #
Disclosed re-derivation: the same two spellings are available in
Provider/ExcessDecay/InteriorEllipticity.lean; they are re-proved here (three
lines each) to keep this module's import cone off the excess-decay boundary
tree, which is under concurrent edit.
2. the display bounding the Λ's by the 𝓔's at CoarseGraining's two ellipticity factors #
The 𝓔-envelope √(2d(𝓔² + 1)) of the display bounding the Λ's by the 𝓔's, at the cube
Q, the family A, the index t and the comparator σ Id.
Equations
- One or more equations did not get rendered due to their size.
Instances For
the display bounding the Λ's by the 𝓔's, lower half. CoarseGraining's
λ_{t,2}^{-1/2} factor is
at most σ^{-1/2} √(2d(𝓔_t² + 1)).
the display bounding the Λ's by the 𝓔's, upper half. CoarseGraining's Λ_{t,2}^{1/2}
factor is at
most σ^{1/2} √(2d(𝓔_t² + 1)).
The envelope in the source's 1 + 𝓔 shape: √(2d(𝓔² + 1)) ≤ √(2d)(1 + 𝓔).
3. The carrier composition: the coarse-graining right-hand side read at the §4.5 data #
The flux-corrected family's coefficient field on any cube is ã_{L,k}.
The §4.5 Dirichlet solution, entered into CoarseGraining's Dirichlet carrier at the
flux-corrected family ã_{L,m} (the field the source's own remark
"the first equation is unchanged if we replace a_L by ã_{L,m}",
licenses).
Equations
Instances For
The ν-drop read at CoarseGraining's price of the entered solution: the left-hand side
of the energy-from-data display.
4. the energy-from-data display #
Step 2a — the energy-from-data display.
For every §4.5 Dirichlet pair (u, h) with forcing g on □_m, every L,
every ω, and every t ∈ (0,1) at which the data are Besov-regular,
ν^{1/2} ‖∇u‖_{L²(□_m)}
≤ C t^{-3/2} · σ_m^{-1/2} √(2d) ( 1 + 𝓔_{t/2,∞,2}(□_m; ã_{L,m}, σ_m) ) · B_g
+ C t^{-1/2} · σ_m^{ 1/2} √(2d) ( 1 + 𝓔_{t,∞,2} (□_m; ã_{L,m}, σ_m) ) · B_h,
C = C(d) CoarseGraining's dimensional constant of the coarse-graining
right-hand side, B_g and B_h the note-normalized Besov data quantities.
The association is (σ^{∓1/2}) · (the 𝓔-bracket); the source writes the
same product as (1 + 𝓔)(σ^{-1/2}·… + σ^{1/2}·…). See the module docstring
for the three disclosed deviations from the printed display.
5. The error carrier: CoarseGraining's 𝓔 IS the flux-corrected error #
The 𝓔 appearing in Step 2a is literally the flux-corrected
error observable's representative (Support.fluxCorrectedError_characterization,
plus isotropicComparatorMatrix σ = scalarMatrix σ by rfl). Recorded so the
Step-2a display and EthmB(m) speak of the same random variable.