JointGridDepthMaximum

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

A joint grid-and-depth Gamma_1 maximum

This file combines the spatial grid entropy and the countable depth entropy before taking any per-depth maximum. If the row at depth k has at most exp (growth * (k + 1)) entries and every entry has a common one-sided Gamma_1 bound at scale a k, then one random envelope controls every row simultaneously at the deterministic price

(growth + 2) * (k + 1) * a k.

The simultaneous domination is necessarily almost everywhere under marginal tail hypotheses. No pointwise conclusion is asserted: the downstream null-set patch is responsible for converting this output into an everywhere statement when that is needed.

The triadic specialization uses growth = d * log 3, since the depth-k row contains exactly 3 ^ (d * (k + 1)) descendants.

def Algsuperdiff.Section3.Provider.CoarseEllipticity.jointDepthEntropyConst (growth : ℝ) : ℝ

The entropy constant which pays for both a row of exponential size and the countable union over depths.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.jointDepthEntropyConst growth = growth + 2

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.jointDepthEntropyConst_pos {growth : ℝ} (hgrowth : 0 ≤ growth) : 0 < jointDepthEntropyConst growth

def Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelopeScale (growth : ℝ) (a : ℕ → ℝ) (k : ℕ) : ℝ

The positive deterministic denominator used to normalize row k.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelopeScale growth a k = Algsuperdiff.Section3.Provider.CoarseEllipticity.jointDepthEntropyConst growth * (↑k + 1) * a k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelopeScale_pos {growth : ℝ} {a : ℕ → ℝ} (hgrowth : 0 ≤ growth) (ha : ∀ (k : ℕ), 0 < a k) (k : ℕ) : 0 < gradedFiniteEnvelopeScale growth a k

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelopeENNReal {Omega : Type u_1} {ι : Type u_2} (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) (growth : ℝ) (omega : Omega) : ENNReal

The extended-valued joint maximum. Keeping this intermediate object makes the countable supremum measurable without first assuming that it is finite.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelope {Omega : Type u_1} {ι : Type u_2} (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) (growth : ℝ) (omega : Omega) : ℝ

The real-valued common envelope. Its almost-everywhere finiteness is a theorem below, not an implicit pointwise consequence of the marginal tails.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelope I X a growth omega = (Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelopeENNReal I X a growth omega).toReal

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelope_nonneg {Omega : Type u_1} {ι : Type u_2} (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) (growth : ℝ) (omega : Omega) : 0 ≤ gradedFiniteEnvelope I X a growth omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_gradedFiniteEnvelope {Omega : Type u_1} {ι : Type u_2} (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) (growth : ℝ) [MeasurableSpace Omega] (hXmeas : ∀ (k : ℕ), ∀ i ∈ I k, Measurable (X k i)) : Measurable (gradedFiniteEnvelope I X a growth)

def Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteRowEvent {Omega : Type u_1} {ι : Type u_2} (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) (growth t : ℝ) (k : ℕ) : Set Omega

The bad event in one finite row at threshold t.

Equations

• One or more equations did not get rendered due to their size.

def Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteAllRowsEvent {Omega : Type u_1} {ι : Type u_2} (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) (growth t : ℝ) : Set Omega

The bad event at any depth at threshold t.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteAllRowsEvent I X a growth t = ⋃ (k : ℕ), Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteRowEvent I X a growth t k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measureReal_gradedFiniteAllRowsEvent_le {Omega : Type u_1} {ι : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) {growth t : ℝ} (hgrowth : 0 ≤ growth) (ht : 1 ≤ t) (hcard : ∀ (k : ℕ), ↑(I k).card ≤ Real.exp (growth * (↑k + 1))) (hX : ∀ (k : ℕ), ∀ i ∈ I k, HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (X k i) (a k)) : mu.real (gradedFiniteAllRowsEvent I X a growth t) ≤ Real.exp (-t)

The spatial and depth entropies are paid in one union bound.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_gammaSigma_one_gradedFiniteEnvelope {Omega : Type u_1} {ι : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) {growth : ℝ} (hgrowth : 0 ≤ growth) (ha : ∀ (k : ℕ), 0 < a k) (hcard : ∀ (k : ℕ), ↑(I k).card ≤ Real.exp (growth * (↑k + 1))) (hX : ∀ (k : ℕ), ∀ i ∈ I k, HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (X k i) (a k)) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (gradedFiniteEnvelope I X a growth) 1

The real common envelope has a unit-scale one-sided Gamma_1 tail.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.ae_gradedFiniteEnvelopeENNReal_ne_top {Omega : Type u_1} {ι : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) {growth : ℝ} (hgrowth : 0 ≤ growth) (ha : ∀ (k : ℕ), 0 < a k) (hcard : ∀ (k : ℕ), ↑(I k).card ≤ Real.exp (growth * (↑k + 1))) (hX : ∀ (k : ℕ), ∀ i ∈ I k, HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (X k i) (a k)) : ∀ᵐ (omega : Omega) ∂mu, gradedFiniteEnvelopeENNReal I X a growth omega ≠ ⊤

The extended joint maximum is finite almost everywhere. This is the precise Borel--Cantelli step which cannot be strengthened to pointwise finiteness from marginal tail assumptions alone.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.ae_le_gradedFiniteEnvelope {Omega : Type u_1} {ι : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) {growth : ℝ} (hgrowth : 0 ≤ growth) (ha : ∀ (k : ℕ), 0 < a k) (hcard : ∀ (k : ℕ), ↑(I k).card ≤ Real.exp (growth * (↑k + 1))) (hX : ∀ (k : ℕ), ∀ i ∈ I k, HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (X k i) (a k)) : ∀ᵐ (omega : Omega) ∂mu, ∀ (k : ℕ), ∀ i ∈ I k, X k i omega ≤ gradedFiniteEnvelopeScale growth a k * gradedFiniteEnvelope I X a growth omega

Almost everywhere, the single envelope simultaneously dominates every member in every row.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gradedFiniteEnvelope_spec {Omega : Type u_1} {ι : Type u_2} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (I : ℕ → Finset ι) (X : ℕ → ι → Omega → ℝ) (a : ℕ → ℝ) {growth : ℝ} (hgrowth : 0 ≤ growth) (ha : ∀ (k : ℕ), 0 < a k) (hcard : ∀ (k : ℕ), ↑(I k).card ≤ Real.exp (growth * (↑k + 1))) (hXmeas : ∀ (k : ℕ), ∀ i ∈ I k, Measurable (X k i)) (hX : ∀ (k : ℕ), ∀ i ∈ I k, HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (X k i) (a k)) : (∀ (omega : Omega), 0 ≤ gradedFiniteEnvelope I X a growth omega) ∧ Measurable (gradedFiniteEnvelope I X a growth) ∧ HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (gradedFiniteEnvelope I X a growth) 1 ∧ ∀ᵐ (omega : Omega) ∂mu, ∀ (k : ℕ), ∀ i ∈ I k, X k i omega ≤ gradedFiniteEnvelopeScale growth a k * gradedFiniteEnvelope I X a growth omega

The reusable generic package: one explicit nonnegative measurable Gamma_1 envelope, with simultaneous almost-everywhere row domination.

The triadic grid specialization

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.triadicJointDepthEntropyConst (d : ℕ) : ℝ

The dimension-only joint entropy constant for triadic descendants.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.triadicJointDepthEntropyConst d = Algsuperdiff.Section3.Provider.CoarseEllipticity.jointDepthEntropyConst (↑d * Real.log 3)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.triadicJointDepthEntropyConst_pos (d : ℕ) : 0 < triadicJointDepthEntropyConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.card_descendantsAtScale_originCube_le_exp (d : ℕ) (m : ℤ) (k : ℕ) : ↑(HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)).card ≤ Real.exp (↑d * Real.log 3 * (↑k + 1))

The exact triadic descendant count, rewritten in exponential-entropy form for the generic joint maximum theorem.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.jointGridDepthEnvelope {Omega : Type u_1} (d : ℕ) (m : ℤ) (X : ℕ → HCPolySupport.TriadicCube d → Omega → ℝ) (a : ℕ → ℝ) : Omega → ℝ

The one random variable which jointly dominates all triadic descendants at all positive scale gaps.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.jointGridDepthEnvelope_spec {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] (d : ℕ) (m : ℤ) (X : ℕ → HCPolySupport.TriadicCube d → Omega → ℝ) (a : ℕ → ℝ) (ha : ∀ (k : ℕ), 0 < a k) (hXmeas : ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), Measurable (X k R)) (hX : ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (X k R) (a k)) : (∀ (omega : Omega), 0 ≤ jointGridDepthEnvelope d m X a omega) ∧ Measurable (jointGridDepthEnvelope d m X a) ∧ HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) (jointGridDepthEnvelope d m X a) 1 ∧ ∀ᵐ (omega : Omega) ∂mu, ∀ (k : ℕ), ∀ R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k), X k R omega ≤ triadicJointDepthEntropyConst d * (↑k + 1) * a k * jointGridDepthEnvelope d m X a omega

The triadic joint grid-and-depth maximum package. One measurable nonnegative Gamma_1 envelope controls every depth and every descendant almost everywhere; the deterministic loss is linear in k + 1 and depends only on the dimension through triadicJointDepthEntropyConst.