OAI/Dynamics/SmoothObstruction/FiniteLaw.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SmoothObstruction.FiniteLaw.Law line 13
2. def OAI.SmoothObstruction.FiniteLaw.expect line 20
3. lemma OAI.SmoothObstruction.FiniteLaw.expect_nonneg line 22
4. lemma OAI.SmoothObstruction.FiniteLaw.expect_mono line 25
5. lemma OAI.SmoothObstruction.FiniteLaw.expect_const line 28
6. lemma OAI.SmoothObstruction.FiniteLaw.expect_add line 31
7. lemma OAI.SmoothObstruction.FiniteLaw.expect_sub line 35
8. lemma OAI.SmoothObstruction.FiniteLaw.expect_mul_const line 39
9. lemma OAI.SmoothObstruction.FiniteLaw.expect_const_mul line 43
10. lemma OAI.SmoothObstruction.FiniteLaw.expect_sum line 47
11. lemma OAI.SmoothObstruction.FiniteLaw.expect_sq_abs line 52
12. def OAI.SmoothObstruction.FiniteLaw.product line 63
13. lemma OAI.SmoothObstruction.FiniteLaw.product_moment line 72
14. lemma OAI.SmoothObstruction.FiniteLaw.product_one_moment line 81
15. lemma OAI.SmoothObstruction.FiniteLaw.product_two_moment line 91
16. def OAI.SmoothObstruction.FiniteLaw.condition line 108
17. lemma OAI.SmoothObstruction.FiniteLaw.condition_bound line 116
18. lemma OAI.SmoothObstruction.FiniteLaw.orthogonal_sum_square line 140
19. lemma OAI.SmoothObstruction.FiniteLaw.centered_square_le line 155
20. lemma OAI.SmoothObstruction.FiniteLaw.empirical_variance line 163

    Source documentation

    The exact second-moment calculation for genuinely independent sampled probability vectors. The vector's coordinates need not be independent.

    lemma empirical_variance [Nonempty I] (P : I → Law A) (Y : I → A → J → ℝ)
        (p : J → ℝ) (hY : ∀ i x a, 0 ≤ Y i x a) (hs : ∀ i x, ∑ a, Y i x a = 1)
        (hm : ∀ i a, expect (P i) (fun x => Y i x a) = p a) :
        (∑ a, expect (product P) (fun x =>
          ((∑ i, Y i (x i) a) / Fintype.card I - p a) ^ 2)) ≤
            1 / Fintype.card I := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.expect, OAI.SmoothObstruction.FiniteLaw.product

21. lemma OAI.SmoothObstruction.FiniteLaw.expected_tv_of_second_moment line 213

    Source documentation

    A finite form of the TV/second-moment inequality, including samples with zero mass.

    lemma expected_tv_of_second_moment (P : Law A) (Z : A → J → ℝ) {v : ℝ}
        (hv : 0 ≤ v) (hvar : ∑ a, expect P (fun x => Z x a ^ 2) ≤ v) :
        expect P (fun x => (1 / 2 : ℝ) * ∑ a, |Z x a|) ≤
          (1 / 2 : ℝ) * Real.sqrt (Fintype.card J * v) := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.expect

22. theorem OAI.SmoothObstruction.FiniteLaw.independent_vectors_tv line 236

    Source documentation

    Source lem:word-tv, for independent complete vectors, with its literal one-half constant. This is used twice, not an assumption about empirical laws.

    theorem independent_vectors_tv [Nonempty I] (P : I → Law A) (Y : I → A → J → ℝ)
        (p : J → ℝ) (hY : ∀ i x a, 0 ≤ Y i x a) (hs : ∀ i x, ∑ a, Y i x a = 1)
        (hm : ∀ i a, expect (P i) (fun x => Y i x a) = p a) :
        expect (product P) (fun x => (1 / 2 : ℝ) *
          ∑ a, |(∑ i, Y i (x i) a) / Fintype.card I - p a|) ≤
            (1 / 2 : ℝ) * Real.sqrt (Fintype.card J / Fintype.card I) := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.expect, OAI.SmoothObstruction.FiniteLaw.product

23. def OAI.SmoothObstruction.FiniteLaw.prob line 253
24. lemma OAI.SmoothObstruction.FiniteLaw.prob_nonneg line 256
25. lemma OAI.SmoothObstruction.FiniteLaw.prob_le_one line 260
26. lemma OAI.SmoothObstruction.FiniteLaw.prob_eq_expect line 265
27. lemma OAI.SmoothObstruction.FiniteLaw.prob_compl line 269
28. lemma OAI.SmoothObstruction.FiniteLaw.markov line 274
29. lemma OAI.SmoothObstruction.FiniteLaw.union_bound line 284
30. lemma OAI.SmoothObstruction.FiniteLaw.good_event_mass line 299
31. lemma OAI.SmoothObstruction.FiniteLaw.exists_good line 318
32. lemma OAI.SmoothObstruction.FiniteLaw.condition_supported line 329
33. def OAI.SmoothObstruction.FiniteLaw.push line 337
34. lemma OAI.SmoothObstruction.FiniteLaw.expect_push line 344