DeGiorgiCoreTwo #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The two-dimensional Sobolev input for De Giorgi iteration #
In dimension two the critical H¹ Sobolev exponent is infinite, so the
d ≥ 3 cube embedding used by the pinned De Giorgi core is unavailable. This
file uses the finite-exponent route instead: first lower H¹ to W¹,⁴⁄³ on
the finite square and then apply the pinned finite-p cube embedding into
L⁴. The resulting factor is L¹⁄², as required by scaling.
The finite exponent 4 / 3 used in the De Giorgi iteration.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The finite exponent 4 used in the De Giorgi iteration.
Equations
- DivergenceFormProcess.Regularity.four = { exponent := 4, one_lt := DivergenceFormProcess.Regularity.four._proof_1, lt_top := DivergenceFormProcess.Regularity.four._proof_2 }
Instances For
The two-dimensional square Sobolev embedding H¹ ↪ L⁴, obtained through
the finite-exponent W¹,⁴⁄³ ↪ L⁴ embedding. The right side is left in its
natural L⁴⁄³ form; the finite-measure comparison to L² is performed in the
next analytic step, where its scale factor is used exactly once.
The two-dimensional matched-pair Sobolev inequality. The scale factor is
written as the exact finite-measure downgrade factor |U|^(1/4); on a square
of side L this is sqrt L.
The two-dimensional matched-pair Sobolev inequality in its scale-normalized form. This is the analytic input used by the two-dimensional level recurrence.