CoarseDatumPricing #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The composed ‖v − h‖_{L²} pricing for a Dirichlet forced solution #
Nothing here imports that file, and nothing here claims the anchor or any source node.
The gap this module closes #
[B] ‖v_cc − h‖_{L²(cc)} ,
where v_cc is CoarseGraining's DirichletForcedCubeSolution on the covering
cube with boundary datum h and force g — the SAME force and the SAME
boundary data as u. This is the author's final same-boundary-data
architecture: nothing is subtracted through the operator anywhere below, and
the zero-trace object is CoarseGraining's own structural zeroTraceDifference
field.
The composition is the manuscript's move 3 at q = 2, with every ingredient
already:
3^{-scale} ‖v − h‖_{L²(Q)}
≤ 2 C_neg(d) [∇(v − h)]_{B^{-s/2}_{2,2}(Q)} (negative norm to L²)
≤ 2 C_neg(d) √2 ( [∇v]_{B^{-s/2}} + [∇h]_{B^{-s/2}} ) (subadditivity)
≤ 2 C_neg(d) √2 ( coarsePoincareWithRHSGradientRHS(s/2)
+ K_s^{1/2} ‖∇h‖_{L²(Q)} ) .
The gradient of the structural zero-trace witness is identified with
∇v − ∇h by uniqueness of the weak gradient (§1), which is the only genuinely
new Lean content of the module.
References #
- ABK26, the Section-2 Caccioppoli lemma's move 3; the boundary application.
- CoarseGraining:
Book/Ch03/Definitions.lean(DirichletForcedCubeSolution),Book/Ch03/Theorems/CoarseCaccioppoli/ZeroTraceValue.lean,Book/Ch03/Theorems/CoarsePoincare.lean,Book/Ch03/Theorems/Energy/Theory.lean,Deterministic/CoarsePoincare/SeminormRecurrence.lean,Deterministic/WeakNormInterfaces/A.lean.
1. The structural zero-trace difference and its gradient #
Uniqueness of the weak gradient in a.e. form.
If two H¹ witnesses on an open set agree a.e., their gradients agree a.e.
This upgrades CoarseGraining's gradCoord_ae_eq_of_toFun_eq (which needs
strict equality of the values) to the a.e. hypothesis actually supplied by
DirichletForcedCubeSolution.zeroTraceDifference.
The value and gradient of the structural zero-trace difference of a
DirichletForcedCubeSolution, in a.e. form on the half-open cube.
2. The composed negative-seminorm pricing #
The dimension-only constant of the composed pricing: the zero-trace value
constant of the negative-norm-to-L² step and the subadditivity factor √2.
Equations
Instances For
The datum difference against the two negative seminorms.
3^{-scale(Q)} ‖v − h‖_{L²(Q)} is bounded by the negative seminorms of ∇v
and of ∇h at the index s/2, at the coefficient-free constant
2 C_neg(d) √2. Both legs are coarse carriers; nothing flat acts on the
solution.
3. The two legs: coarse Poincaré on v, crude Jensen on h #
The ForcedCubeSolution adapter: a Dirichlet forced solution is a forced
solution, at the same force, by forgetting the boundary datum.
Equations
- Algsuperdiff.Section4.Provider.ExcessDecay.forcedOfDirichlet v = { toH1 := v.toH1, weakSolution := ⋯ }
Instances For
The gradient leg of the solution, in the explicit coarse display at the r₀ = s/2 pin. This is coarsePoincareRHSTheory clause (i) read through the public/internal
Besov bridge.
4. The composed pricing #
The composed datum pricing. The pricing of the structural datum difference of a Dirichlet forced solution, in its displayed shape:
3^{-scale(Q)} ‖v − h‖_{L²(Q)}
≤ C₁ ( (s/2)^{-3/2} λ_{s/4,2}^{-1/2} · dirichletEnergyWithRHSRHS(C₂, s/2)
+ (s/2)^{-3} λ_{s/4,2}^{-1} [g]_{B^{s/2}_{2,2}(Q)}
+ K_s^{1/2} ‖∇h‖_{L²(Q)} ) .
All three legs are coarse (λ-weighted) except the last, which acts on the
datum h alone. Nothing is subtracted through the operator: the force is
g at every station and the zero-trace object is CoarseGraining's own
structural zeroTraceDifference.