OAI/Analysis/Littlewood/DependentMoments.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_singleton line 17
2. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_independent_selections line 22
3. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_double_selections line 29
4. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_fst line 56
5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_snd line 62
6. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.bad_pair_avg_bound line 69
7. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.selections_variance line 106

   Source documentation

   A finite dependent-row moment estimate. Dependence is charged only to same-chunk collisions; rows on distinct chunks use independent coordinates.

   lemma selections_variance (f : J → Y → (κ → A) → ℝ)
       (c : Y → J → κ) (a : Y → J → A) (good : Y → Prop)
       [DecidablePred good] {b d : ℝ}
       (hf : ∀ j y ω, 0≤f j y ω ∧ f j y ω≤1)
       (hc : ∀ y, good y → Function.Injective (c y))
       (ha : ∀ y, good y → ∀ j ω,
         f j y ω=(if ω (c y j)=a y j then 1 else 0))
       (hb : avg (fun y ↦ if good y then 0 else 1)≤b)
       (hd : avg (fun yy : Y × Y ↦
         if ∃ j l, c yy.1 j=c yy.2 l then 1 else 0)≤d) :
       avg (fun ω : κ → A ↦
         (avg (fun y ↦ ∏ j, f j y ω)-(1/(Fintype.card A : ℝ))^(Fintype.card J))^2)
   …

   Mentions: OAI.AsymptoticallyMinimalLittlewood.Packing.avg

8. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_finset line 153
9. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_fibers line 162
10. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_fiber_event line 181
11. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_uniform_event line 204
12. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_cross_chunks line 217
13. def OAI.AsymptoticallyMinimalLittlewood.Packing.rowsGood line 248
14. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.sum_form_surjective line 255
15. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.sub_form_surjective line 264
16. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.rowsGood_injective line 273
17. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.rows_bad_indicator line 284
18. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_bad_rows line 325
19. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_cross_rows line 363
20. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.averaged_density_variance line 400

    Source documentation

    Averaging over the anchored coordinate removes even the exceptional centers. This quantitative statement is used before pruning the slot graph.

    lemma averaged_density_variance (f : V →ₗ[K] K) (g : J → V →ₗ[K] K)
        (hf : Function.Surjective f)
        (hg : ∀ j, Function.Surjective (g j))
        (hfg : ∀ j, Function.Surjective (f.prod (g j)))
        (hpair : ∀ j l, j≠l → Function.Surjective ((g j).prod (g l)))
        (G S : Finset K) (chunk : K → κ)
        (hchunk : ∀ t∈G, ∀ u∈G, chunk t=chunk u → t+u∈S ∨ t-u∈S)
        (hit : J → K → (κ → A) → Prop) [∀ j t ω, Decidable (hit j t ω)]
        (hhit : ∀ j t, t∈G → ∃ a : A, ∀ ω, hit j t ω ↔ ω (chunk t)=a)
        {B : ℝ} (hB : ∀ k, ((Finset.univ.filter (fun t : K ↦ chunk t=k)).card : ℝ)≤B) :
        avg (fun ω : κ → A ↦ avg (fun s : K ↦
          (avg (fun y : fiber f s ↦ ∏ j, if hit j (g j y) ω then (1 : ℝ) else 0)-
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Packing.avg, OAI.AsymptoticallyMinimalLittlewood.Packing.fiber

21. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.exists_few_bad_centers_total line 457
22. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.exists_few_bad_centers_averaged line 477