StoppingLabelWeights.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit logarithmic aggregation costs for the actual finite stopping labels on a fixed dilation of X. The inverse-binomial scalar is retained, and the bounds apply to every early or late subset of labels.

theorem OAI.CubicFirstMoment.stoppingLabelBox_card_fixed line 14
theorem OAI.CubicFirstMoment.stoppingLabelBox_card_dilated line 38

theorem OAI.CubicFirstMoment.stopping_label_weighted_sum_dilated line 61

Source documentation

One constant covers arbitrary early/late label subsets and every family of piece bounds. In particular, no sign is discarded from a piece.

theorem stopping_label_weighted_sum_dilated {ρ c : ℝ} (hρ : 1 < ρ) (hc : 1 ≤ c) :
    ∃ K : ℝ, 0 < K ∧ ∀ X : ℝ, 1 ≤ X →
      ∀ I : Finset (ℕ × ℕ × ℕ), I ⊆ stoppingLabelBox ρ (c*X) →
      (I.card:ℝ) ≤ K*(1+Real.log X)^3 ∧
      ∀ (f : (ℕ × ℕ × ℕ) → ℂ) (M : ℝ), 0 ≤ M →
        (∀ q ∈ I, ‖f q‖ ≤ M) →
        ‖∑ q ∈ I, (Nat.choose (q.2.1+q.2.2) q.2.1:ℂ)⁻¹*f q‖ ≤
          K*(1+Real.log X)^3*M := by
…

Mentions: OAI.CubicFirstMoment.stoppingLabelBox

lemma OAI.CubicFirstMoment.stopping_early_labels_subset line 87
theorem OAI.CubicFirstMoment.stopped_norm_partition_subset_count line 93
Source documentation
The low distinguished-scale restriction can only lower the number of norm-partition indices; its exact cutoff need not be relaxed.
```
theorem stopped_norm_partition_subset_count (i : ℕ) :
    ∃ D : ℝ, 0 < D ∧ ∀ X : ℝ, 1 ≤ X →
      ∀ I : Finset (Fin i → Fin (normPartitionCount (Real.exp primeProductWeights.radius*X))),
        (I.card:ℝ) ≤ D*(1+Real.log X)^i := by
…
```
Mentions: OAI.CubicFirstMoment.normPartitionCount