FiniteLayercake.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A finite positive layer decomposition for the diagonal ratio

theorem OAI.Ostmann.finite_level_sum_norm_bound line 14

Source documentation

Uniform bounds on all upper level sums control every nonnegative bounded multiplier with no loss depending on the number of sampled values.

theorem finite_level_sum_norm_bound {A : Type*} (S : Finset A)
    (r : A → ℝ) (c : A → ℂ) (M δ : ℝ)
    (hM : 0 ≤ M) (hδ : 0 ≤ δ)
    (hr : ∀ a ∈ S, 0 ≤ r a ∧ r a ≤ M)
    (hlevel : ∀ t : ℝ, 0 < t → ‖∑ a ∈ S, if t ≤ r a then c a else 0‖ ≤ δ) :
    ‖∑ a ∈ S, (r a : ℂ) * c a‖ ≤ M * δ := by
…

theorem OAI.Ostmann.finite_product_ratio_norm_bound line 78

Source documentation

The normalized reciprocal product costs no additional constant once the same correlation bound holds with arbitrary product upper cutoffs.

theorem finite_product_ratio_norm_bound {A : Type*} (S : Finset A)
    (H : A → ℝ) (c : A → ℂ) (X δ : ℝ) (hX : 0 < X) (hδ : 0 ≤ δ)
    (hH : ∀ a ∈ S, X ≤ H a)
    (hcut : ∀ R : ℝ, ‖∑ a ∈ S, if H a ≤ R then c a else 0‖ ≤ δ) :
    ‖∑ a ∈ S, ((X / H a : ℝ) : ℂ) * c a‖ ≤ δ := by
…

theorem OAI.Ostmann.finite_product_ratio_norm_bound_on_support line 104

Source documentation

Zero coefficients can carry arbitrary product values. Only the original supported terms need the lower product range.

theorem finite_product_ratio_norm_bound_on_support {A : Type*} (S : Finset A)
    (H : A → ℝ) (c : A → ℂ) (X δ : ℝ) (hX : 0 < X) (hδ : 0 ≤ δ)
    (hsupport : ∀ a ∈ S, c a ≠ 0 → X ≤ H a)
    (hcut : ∀ R : ℝ, ‖∑ a ∈ S, if H a ≤ R then c a else 0‖ ≤ δ) :
    ‖∑ a ∈ S, ((X / H a : ℝ) : ℂ) * c a‖ ≤ δ := by
…