BulkLogJointComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Joint replacement of the original bulk-prime samples

Every slice error is derived from the published progression estimate. The commuting coordinate averages give the full product comparison with the retained Page measures; no independence of a conditionally sampled weight is assumed.

theorem OAI.Ostmann.PublishedProgressionInput.bulk_log_joint_comparison line 19

Source documentation

Product comparison for the actual smooth tree, on arbitrary distinct bulk coordinates and arbitrary residue cells.

theorem PublishedProgressionInput.bulk_log_joint_comparison
    (P : PublishedProgressionInput) {σ : Type*} [Fintype σ]
    (base : σ → ℝ) (order : List σ) (horder : order.Nodup)
    {n : ℕ} (T : MovingSlotData σ n) (hT : ∀ i ∈ order, T.CompensationAbsent i)
    (i₀ : σ) (hi₀ : i₀ ∈ order) (ψ : 𝓢(ℝ, ℂ)) (X lo hi V : ℝ)
    (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (hV : T.Frequencies (fun s => |(s : ℝ)| ≤ V))
    (φ : ℝ → ℝ) (G : ℕ → ℝ) (B D : ℝ) (hB : 0 ≤ B) (hD : 0 ≤ D)
    (hφ : ∀ x, |φ x| ≤ B) (hlip : ∀ x y, |φ x - φ y| ≤ D * |x - y|)
    (hout : ∀ x, 1 ≤ |x| → φ x = 0)
    (d r : ℕ) (hsize : T.SizeLE d) (hregular : T.RegularLengthLE r) (L R : ℝ)
    (Q : ℕ) (hQ : 2 ≤ Q) (q a : σ → ℕ) (u v : σ → ℝ)
    (hu : ∀ i, 1 ≤ u i) (hq : ∀ i ∈ order, 1 ≤ q i)
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MovingSlotData