UpperCommonEnvelope

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

Finite-q upper aggregation from one common random envelope

This file isolates the valid joint-probability input needed after UpperPolyProfile.lean. Marginal Gamma_1 certificates for a family U n do not, by themselves, give a q-uniform certificate for its weighted ell^(q/2) aggregate: at large finite q the aggregate can see the maximum of many unrelated variables. The usable input is instead one common nonnegative envelope V, with

U n omega <= upperPolyProfile A gamma n * V omega

simultaneously for every depth. The random factor then leaves the entire aggregate before any depth summation. The deterministic theorem upperPolyProfile_aggregate_le_of_two_le supplies the source's cubic budget, uniformly in finite q >= 2, and scaling the single Gamma_1 certificate for V supplies the joint random lane.

The theorem here is conditional: it does not manufacture the common envelope. Producing it requires a joint grid-and-depth maximum estimate from the model-facing upper block bound. In particular, no family of marginal tail bounds is accepted as a substitute.

Source and provenance

• ABK26, for the ordinary upper profile and cubic pole.
• UpperPolyProfile.lean, for the deterministic finite-q aggregation.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_geometricWeight_mul_upperPolyProfile_rpow_of_two_le {A gamma s q : ℝ} (hA : 0 ≤ A) (hgamma : 0 ≤ gamma) (hs : 0 < s) (hs1 : s ≤ 1) (hq : 2 ≤ q) (hgap : 0 < 2 * s - gamma) : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s q n * upperPolyProfile A gamma n ^ (q / 2)

The quadratic upper profile has a summable weighted q/2 power on the source window. This is the summability companion to upperPolyProfile_aggregate_le_of_two_le.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperPolyProfile_aggregate_le_commonEnvelope {Omega : Type u_1} {U : ℕ → Omega → ℝ} {V : Omega → ℝ} {A gamma s q : ℝ} (hA : 0 ≤ A) (hgamma : 0 ≤ gamma) (hs : 0 < s) (hs1 : s ≤ 1) (hq : 2 ≤ q) (hgap : 0 < 2 * s - gamma) (hUnonneg : ∀ (n : ℕ) (omega : Omega), 0 ≤ U n omega) (hVnonneg : ∀ (omega : Omega), 0 ≤ V omega) (hdom : ∀ (n : ℕ) (omega : Omega), U n omega ≤ upperPolyProfile A gamma n * V omega) (omega : Omega) : (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * U n omega ^ (q / 2)) ^ (2 / q) ≤ 384 * A * s * (2 * s - gamma)⁻¹ ^ 3 * V omega

A simultaneous pointwise upper-profile envelope factors out of the full weighted ell^(q/2) aggregate. This is a deterministic statement; its quantifier forall n omega is the essential joint input.