OAI/Analysis/Littlewood/Averages.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AsymptoticallyMinimalLittlewood.Packing.avg line 16
2. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_const line 18
3. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_add line 21
4. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_sub line 24
5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_mul_const line 27
6. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_const_mul line 30
7. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_mono line 33
8. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_nonneg line 35
9. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_sum line 38
10. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_abs line 43
11. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.exists_le_avg line 47
12. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_comm line 55
13. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_prod_type line 63
14. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_prod_coordinate line 68
15. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_prod_injective line 74
16. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_error_on_bad line 105

    Source documentation

    Good configurations contribute exactly c; all bad configurations carry only a bounded contribution. This is the uniform first/second moment input.

    lemma avg_error_on_bad (f : Ω → ℝ) (good : Ω → Prop) [DecidablePred good]
        {c : ℝ} (hc : 0≤c) (hc1 : c≤1) (hf : ∀ ω, 0≤f ω ∧ f ω≤1)
        (he : ∀ ω, good ω → f ω=c) :
        |avg f-c| ≤ avg (fun ω ↦ if good ω then 0 else 1) := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Packing.avg

17. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_square_error line 117
18. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_chebyshev line 132
19. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_mul_avg line 143
20. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_square line 150
21. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.moments_from_good line 158

    Source documentation

    Unconditional moments suffice: pruning all atypical candidate centers only enlarges the deleted set, so no conditional-probability axiom is used.

    lemma moments_from_good {Y : Type uY} [Fintype Y] [Nonempty Y]
        (f : Y → Ω → ℝ) (good : Y → Prop) (good₂ : Y × Y → Prop)
        [DecidablePred good] [DecidablePred good₂] {p a : ℝ}
        (hp : 0≤p) (hp1 : p≤1) (hf : ∀ y ω, 0≤f y ω ∧ f y ω≤1)
        (hfirst : ∀ y, good y → avg (f y)=p)
        (hsecond : ∀ yy, good₂ yy → avg (fun ω ↦ f yy.1 ω*f yy.2 ω)=p^2)
        (hbad : avg (fun y ↦ if good y then 0 else 1)≤a)
        (hbad₂ : avg (fun yy ↦ if good₂ yy then 0 else 1)≤a) :
        avg (fun ω ↦ (avg (fun y ↦ f y ω)-p)^2) ≤ 3*a := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Packing.avg

22. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.exists_few_bad_centers line 182
23. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_indicator line 203
24. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.avg_bad_union line 209