FiniteQLtTwoPresplit

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The conditional finite-q < 2 pre-split producer

This file implements the corrected sublinear route for the finite lower coarse-ellipticity aggregate when 1 <= q < 2. At each depth, the random remainder is written as a n * V n, where a n is its deterministic Orlicz amplitude and V n = O_{Gamma_sigma}(1) is normalized. The probability weights

c n = w n * (a n)^(q/2) / sum_k w k * (a k)^(q/2)

then permit Jensen's inequality without replacing the source weight by a slower one. This is essential: direct linearization against w n would need the stronger, non-source restriction s * q > gamma. The normalized route uses only 2 * s > gamma and retains the corrected pole of order 2 / q.

Main results

• tsum_weighted_rpow_root_le_of_one_le_of_le_two: countable weighted Jensen for exponents 1 <= q <= 2 and subprobability weights.
• twoTermFamilySplit_cutoffLowerEllipticityInv_of_finiteQLtTwoPresplit: the exact finite-q cutoff aggregate split into its corrected deterministic profile and a normalized random lane.
• coarse_ellipticity_lower_branchPayload_lt_two_of_finiteQPresplit: the corresponding payloadLtTwo interface of LowerLegProfile.lean.

Conditional status and A inventory

This file proves only a local aggregation result. It does not itself prove the analytic producer finiteQPresplit, and carries no source-node status. The concrete downstream superposed-flux provider supplies that producer and proves the lower leg; a separate downstream provider proves the upper leg. In the main theorem, hdepth, hVO, and hbudget are explicit analytic A obligations: the per-depth deterministic-plus-random estimate and its Orlicz control. The wrapper's finiteQPresplit input is the same conditional analytic producer, uniformly over the induction data. Relative to an exact source-facing theorem these are proof obligations to discharge, not source premises. The other inputs record the standing model, dimension, positivity, measurability, and summability; the corrected 2 / q pole and random depth-zero lane are the adopted mathematical form. No induction hypothesis is altered or unpacked here.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_weighted_rpow_root_le_of_one_le_of_le_two {q : ℝ} {w H : ℕ → ℝ} (hq1 : 1 ≤ q) (hq2 : q ≤ 2) (hw : ∀ (n : ℕ), 0 ≤ w n) (hH : ∀ (n : ℕ), 0 ≤ H n) (hwsum : Summable w) (hwone : ∑' (n : ℕ), w n ≤ 1) (hWHsum : Summable fun (n : ℕ) => w n * H n) (hWqsum : Summable fun (n : ℕ) => w n * H n ^ (q / 2)) : (∑' (n : ℕ), w n * H n ^ (q / 2)) ^ (2 / q) ≤ ∑' (n : ℕ), w n * H n

Countable weighted Jensen for the sublinear power q / 2. The weights may have total mass at most one; this is the form used after normalizing the per-depth Orlicz amplitudes.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_add_le_two_mul_add_rpow_of_one_le_of_le_two {x y p : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hp1 : 1 ≤ p) (hp2 : p ≤ 2) : (x + y) ^ p ≤ 2 * (x ^ p + y ^ p)

Two nonnegative terms incur at most a factor two for exponents between one and two.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.rpow_add_le_two_mul_add_rpow {a b q : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hq1 : 1 ≤ q) (hq2 : q ≤ 2) : (a + b) ^ (2 / q) ≤ 2 * (a ^ (2 / q) + b ^ (2 / q))

The root exponent 2 / q is at most two when 1 <= q; hence its two-term convexity loss is bounded by the fixed factor two.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.twoTermFamilySplit_cutoffLowerEllipticityInv_of_finiteQLtTwoPresplit {d : ℕ} (M : ABKModel d) (m : ℤ) (r : { r : ℝ // 1 ≤ r }) (hr : ↑r < 2) {s Cprof scaling sigmaTail B : ℝ} (hs : 0 < s) (hgap : 0 < 2 * s - M.gamma) (hCprof : 0 ≤ Cprof) (hscaling : 0 ≤ scaling) (hsigmaTail : 0 < sigmaTail) {L0 : ℤ} {V : ℕ → Cutoff.CutoffSample d → ℝ} {a : ℕ → ℝ} (hVnonneg : ∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ V n omega) (hVmeas : ∀ (n : ℕ), Measurable (V n)) (ha : ∀ (n : ℕ), 0 < a n) (hasum : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2)) (hVlinsum : ∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2) * V n omega) (hVO : ∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigmaTail) (V n) 1) (hbudget : 2 * (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2)) ^ (2 / ↑r) * HCPolySupport.IndependentSums.gammaTriangleConst sigmaTail ≤ B) (hdepth : ∀ (omega : Cutoff.CutoffSample d) (L : ℤ), L0 ≤ L → ∀ (n : ℕ), scaling * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega) ≤ finiteQGeometricProfile Cprof M.gamma n + a n * V n omega) : ∃ (Ydet : Cutoff.CutoffSample d → ℝ) (Y : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d) (L : ℤ), L0 ≤ L → Observable.cutoffLowerEllipticityInv M m L s hs (CoarseEllipticityExponent.finite r) omega * scaling ≤ Ydet omega + Y omega) ∧ (∀ (omega : Cutoff.CutoffSample d), Ydet omega ≤ 8 * Cprof * (s / (2 * s - M.gamma)) ^ (2 / ↑r)) ∧ Measurable Y ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma sigmaTail) Y B

A normalized per-depth finite-q < 2 split produces the lower coarse-ellipticity two-slot payload. The amplitude profile stays inside the exact ell^(q/2) aggregate; only its normalized probability weights are linearized.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarse_ellipticity_lower_branchPayload_lt_two_of_finiteQPresplit (d : ℕ) {Clow Cprof : ℝ} (hCprof : 0 ≤ Cprof) (habsorb : 8 * Cprof ≤ Clow) (finiteQPresplit : ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (r : { r : ℝ // 1 ≤ r }), ↑r < 2 → ∀ s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1, ∃ (V : ℕ → Cutoff.CutoffSample d → ℝ) (a : ℕ → ℝ), (∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ V n omega) ∧ (∀ (n : ℕ), Measurable (V n)) ∧ (∀ (n : ℕ), 0 < a n) ∧ (Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2)) ∧ (∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2) * V n omega) ∧ (∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (V n) 1) ∧ 2 * (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2)) ^ (2 / ↑r) * HCPolySupport.IndependentSums.gammaTriangleConst ((1 - sigma) / 2) ≤ Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)) ∧ ∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → ∀ (n : ℕ), ↑(Annealed.sigmaBar M (m - 1)) * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega) ≤ finiteQGeometricProfile Cprof M.gamma n + a n * V n omega) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) : Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (r : { r : ℝ // 1 ≤ r }), ↑r < 2 → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), ∃ (Ydet : Cutoff.CutoffSample d → ℝ) (Y : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → Observable.cutoffLowerEllipticityInv M m L s ⋯ (CoarseEllipticityExponent.finite r) omega * ↑(Annealed.sigmaBar M (m - 1)) ≤ Ydet omega + Y omega) ∧ (∀ (omega : Cutoff.CutoffSample d), Ydet omega ≤ Clow * (s / (2 * s - M.gamma)).rpow (2 / ↑r)) ∧ Measurable Y ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) Y (Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

The normalized finite-q < 2 pre-split interface discharges exactly the payloadLtTwo argument of coarse_ellipticity_lower_payload_of_branchPayloads.

The gate 8 * Cprof <= Clow absorbs the factor four reconciling the exact geometric profile with the frozen base and the factor two from taking the convex outer root. The analytic producer remains explicit in this helper; the downstream superposed-flux caller supplies the per-depth normalized remainders and their Orlicz amplitude profile.