OAI/Probability/ThorpShuffle/FirstMoment.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Thorp.Current.reciprocalFirst line 13

   Source documentation

   The FIRST reciprocal degree moment of the concrete symmetric-group irreducible family. Specht.degree is the actual complex dimension.

   Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:197 (same declaration text).

   def reciprocalFirst (n : ℕ) : ℝ :=
   …

2. def OAI.Thorp.Current.exceptionalFirst line 19

   Source documentation

   Exactly the non-row, non-column shapes: defect is size minus the maximum of first row length and first column length. For size≥1 defect=0 precisely for the row or column; at size=1 they coincide and are counted once.

   Also declared: ComparatorChallenges/ThorpFirstReciprocal.lean:200 (same declaration text).

   def exceptionalFirst (n : ℕ) : ℝ :=
   …

3. def OAI.Thorp.Current.C1 line 23

   Source documentation

   The supremum of the first reciprocal degree moments over positive sizes. Boundedness is proved in reciprocal_degrees.

   Distinct definitions of this name: ComparatorChallenges/ThorpFirstReciprocal.lean:203 (same statement text; different proof or body). Qualify references as OAI.Thorp.Current.C1@path.

   def C1 : ℝ := sSup (Set.range (fun n : {n : ℕ // 1 ≤ n} => reciprocalFirst n.val))
   …

   Mentions: OAI.Thorp.Current.reciprocalFirst

4. lemma OAI.Thorp.Current.partition_first_exponential_decay line 28
5. def OAI.Thorp.Current.inverseFirst line 68
6. def OAI.Thorp.Current.slice line 70
7. def OAI.Thorp.Current.smallSlice line 72
8. lemma OAI.Thorp.Current.inverseFirst_nonneg line 75
9. lemma OAI.Thorp.Current.slice_nonneg line 76
10. lemma OAI.Thorp.Current.smallSlice_nonneg line 77
11. lemma OAI.Thorp.Current.slice_bound line 79
12. lemma OAI.Thorp.Current.smallSlice_bound line 90
13. lemma OAI.Thorp.Current.smallSlice_tendsto line 105
14. lemma OAI.Thorp.Current.smallSum_tendsto line 124
15. lemma OAI.Thorp.Current.smallSlice_as_sum line 137
16. lemma OAI.Thorp.Current.smallSlice_support line 157
17. lemma OAI.Thorp.Current.smallSum_eq line 162
18. lemma OAI.Thorp.Current.bulkSum_bound line 176
19. lemma OAI.Thorp.Current.exceptionalFirst_split line 197
20. theorem OAI.Thorp.Current.exceptionalFirst_tendsto line 208

    Source documentation

    The contribution of positive-defect Specht modules tends to zero.

    theorem exceptionalFirst_tendsto : Tendsto exceptionalFirst atTop (𝓝 0) := by
    …

    Mentions: OAI.Thorp.Current.exceptionalFirst

21. lemma OAI.Thorp.Current.reciprocalFirst_nonneg line 222
22. lemma OAI.Thorp.Current.full_reciprocalFirst_bound line 225
23. lemma OAI.Thorp.Current.reciprocalFirst_bddAbove line 249

    Source documentation

    Uniform first-moment bound, including the finitely many initial sizes.

    lemma reciprocalFirst_bddAbove :
        BddAbove (Set.range (fun n : {n : ℕ // 1 ≤ n} => reciprocalFirst n.val)) := by
    …

    Mentions: OAI.Thorp.Current.reciprocalFirst

24. lemma OAI.Thorp.Current.reciprocalFirst_le_C1 line 256
25. lemma OAI.Thorp.Current.C1_nonneg line 259
26. theorem OAI.Thorp.Current.reciprocal_degrees line 262