LowerLegProfile #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The all-q unification of the lower leg's deterministic profile #
The frozen lower display of p.cg.ellipticity.bounds quantifies over every
admissible exponent q in [1, infinity] and puts its deterministic shift in one
slot, lowerEllipticityProfile Ccg gamma s q (Section3/Exponent.lean). That
one symbol is the union of three distinct source facts, and this module makes
the union explicit, without touching the frozen shape:
| branch | profile value | source status |
|---|---|---|
finite q < 2 | C (s (2s-gamma)^{-1})^{2/q} | --- the printed order-one pole is false below |
q = 2; the corrected order is 2/q | ||
finite 2 <= q | C s (2s-gamma)^{-1} | --- the printed pole's shape is confirmed; the payload |
| remains a conditional input of this module | ||
q = infinity | C | e.coarse.grained.ellipticity.infty: no pole |
coarse_ellipticity_lower_payload_of_branchPayloads recombines three
branch-indexed payloads into the single all-q payload that
Provider/CoarseEllipticity/LowerLeg.lean's reduction consumes. The
downstream theorem superposedFlux_coarse_ellipticity_lower_leg now supplies
all three branches; this module retains the conditional decomposition.
Where the branch boundary comes from, and what q < 2 really needs #
lambda_{s,q}^{-1} is an ell^{q/2}-type aggregation of the per-scale grid
maxima. A linear weighted-series bound --- "the target is at most
sum_k w_k G_k" --- is available exactly when ell^1 norm-embeds in
ell^{q/2} (‖·‖_{ℓ^{q/2}} ≤ ‖·‖_{ℓ¹}), i.e. exactly when q/2 >= 1
(direction corrected). That is where the boundary at q = 2 comes from, and
it is why the two finite branches are produced by different arguments, both of
them outside this module: coarse_ellipticity_lower_branchPayload_two_le_of_finiteQPresplit
(FiniteQPresplit.lean) on 2 <= q, and
coarse_ellipticity_lower_branchPayload_lt_two_of_finiteQPresplit
(FiniteQLtTwoPresplit.lean) on q < 2, at the corrected order 2/q.
The boundary itself is inherited from the proved lowerEllipticityProfile's
case split (Section3/Exponent.lean), which is read off branch by branch
below; what this module adds is the exhaustiveness of the three branches, so
that a caller holding all three payloads holds the all-q one.
What is proved here #
coarseEllipticityExponent_trichotomy--- the admissible exponent carrier is a covering by the three source branches (exhaustiveness is what is proved; disjointness is not needed and not claimed ---).lowerEllipticityProfile_finite_of_lt_two,lowerEllipticityProfile_finite_of_two_le,lowerEllipticityProfile_infinity--- the three profile values, read off the frozen statement's raw parameters branch by branch.rpow_two_mul_div_le--- the constant reconciliation of the correctedq < 2leg: the two renderings of its base differ by2^{2/r} <= 4, a dimension-only factor, because every admissible exponent satisfies1 <= r.coarse_ellipticity_lower_payload_of_branchPayloads--- the unification: three branch payloads give the all-qpayload ofcoarse_ellipticity_lower_leg_body_of_familySplitPayload.
What is not proved in this module #
This module does not itself produce any of the three branch payloads. They
remain explicit inputs of the unification. The downstream superposed-flux
provider supplies the branch payloads and proves
superposedFlux_coarse_ellipticity_lower_leg; the separate downstream theorem
superposedFlux_coarse_ellipticity_upper_leg supplies the upper leg, and the
now-proved frozen export consumes both through the assembly theorem. In
particular the q < 2 branch payload is not derived from
the 2 <= q one: on the frozen window the two profiles are incomparable (the
base s/(2s - gamma) exceeds one exactly when s <= gamma, and the frozen
window s in [gamma/2 + exp(...), 1] contains points on both sides), so neither
branch implies the other.
References #
- ABK26,
p.cg.ellipticity.bounds, statement, proof; the coarse-grained ellipticity constants.
1. The three source branches of the admissible exponent carrier #
The admissible exponent carrier of the frozen statement is exactly the union of the three source branches: finite below two, finite at least two, and the infinity endpoint.
The deterministic lower profile on the frozen statement's raw parameters, in
the corrected finite q < 2 branch.
The deterministic lower profile at the infinity endpoint: the direct constant, with no pole.
2. The constant reconciliation of the corrected q < 2 leg #
3. The all-q unification #
The all-q lower payload from its three source branches.
The frozen display's single deterministic slot
lowerEllipticityProfile Clow gamma s q is the union of three distinct source
facts; this theorem is the union, and nothing else. Its output is verbatim the
payload binder of coarse_ellipticity_lower_leg_body_of_familySplitPayload,
so composing the two proves the local lower-leg result from the three branches.
All three inputs remain explicit obligations of this helper; a concrete
downstream caller supplies them in the proof of
superposedFlux_coarse_ellipticity_lower_leg.