WholeBallConcentration.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactModuli.KW.whole_ball_estimate line 17
def OAI.ExactModuli.KW.oldCombination line 78
lemma OAI.ExactModuli.KW.integrable_oldCombination line 82

theorem OAI.ExactModuli.KW.whole_ball_approximation line 89

Source documentation

Whole-ball approximation for arbitrary coefficients, after fixing the multiplier law, and before choosing the number of copies.

theorem whole_ball_approximation {p r q h : ℝ} (hp : 1 < p) (hpmax : p ≤ 3/2)
    (hr : 0 < r) (hq : 0 < q) (hh : 0 < h)
    (hmq : (Fintype.card κ : ℝ) * q < 1)
    (herr : (Fintype.card κ : ℝ) * q + h⁻¹ *
      (2 * (Fintype.card κ : ℝ) * r + (1 - (Fintype.card κ : ℝ) * q)⁻¹ - 1) < h)
    (hpq : 10 * (108 * scale p / r) ^ p < q)
    {x : B → ℝ} {u : κ → B → ℝ} (hx : Integrable x μ) (hu : ∀ k, Integrable (u k) μ)
    (hun : ∀ k, ∫ b, |u k b| ∂μ = 1) (a : κ → ι → ℝ)
    (hg : ∫ z, |enlargedFunction p x u a z| ∂(μ.prod (arrayMeasure κ ι)) ≤ 1) :
    ∃ c : κ → ℝ,
      (∫ b, |normalizeFunction μ (oldCombination x u c) b| ∂μ) ≤ 1 ∧
      (μ.prod (arrayMeasure κ ι)).real
…

Mentions: OAI.ExactModuli.KW.scale, OAI.ExactModuli.KW.enlargedFunction, OAI.ExactModuli.KW.arrayMeasure, OAI.ExactModuli.KW.normalizeFunction, OAI.ExactModuli.KW.oldCombination

lemma OAI.ExactModuli.KW.enlargement_parameters line 151