WholeBallCoefficients.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactModuli.KW.enlargedFunction line 18
Source documentation
The representation used in the whole-ball argument.
```
def enlargedFunction (p : ℝ) (x : B → ℝ) (u : κ → B → ℝ) (a : κ → ι → ℝ)
    (z : B × (κ → cube ι)) : ℝ :=
…
```
Mentions: OAI.ExactModuli.KW.cube
lemma OAI.ExactModuli.KW.measurable_enlargedFunction line 22
lemma OAI.ExactModuli.KW.integrable_enlargedFunction line 30
lemma OAI.ExactModuli.KW.resampling_difference line 41

theorem OAI.ExactModuli.KW.coefficient_bound_108 line 60

Source documentation

Resampling controls the coefficients of EVERY representation of a point of the new unit ball.

theorem coefficient_bound_108 {p : ℝ} (hp : 1 < p) (hpmax : p ≤ 3/2)
    {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)
    (k : κ) : coefficientNorm p (a k) ≤ 108 := by
…

Mentions: OAI.ExactModuli.KW.enlargedFunction, OAI.ExactModuli.KW.arrayMeasure, OAI.ExactModuli.KW.coefficientNorm

lemma OAI.ExactModuli.KW.concentration_center line 100

Source documentation

Averaging over the resampled copy produces a deterministic center.

lemma concentration_center {R : Type uR} [MeasurableSpace R] {ν : Measure R}
    [IsProbabilityMeasure ν] {z : R → ℝ} (hz : Measurable z) {r q : ℝ}
    (h : (ν.prod ν).real {v | r < |z v.1 - z v.2|} < q) :
    ∃ c : ℝ, ν.real {v | r < |z v - c|} < q := by
…

lemma OAI.ExactModuli.KW.diffRowSum_prod_tail line 128
lemma OAI.ExactModuli.KW.rowSum_concentration line 144
lemma OAI.ExactModuli.KW.abs_add_lower line 159