OAI/Probability/CubeShuffle/ShapeSpectral.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubeShuffle.DimensionEstimates.medium_parameters line 11
2. lemma OAI.CubeShuffle.Specht.dimension_pos line 31
3. lemma OAI.CubeShuffle.Specht.near_numerical_cutoff line 38
4. lemma OAI.CubeShuffle.Specht.near_row_amplification line 61
5. theorem OAI.CubeShuffle.Specht.near_row_spectral line 82

   Source documentation

   Uniform near-row decay for the actual full-permutation palindrome. The tuple size and fixed-space multiplicity are constructed, not assumed.

   theorem near_row_spectral :
       ∃ X : ℝ, 2 ≤ X ∧ ∀ (d : ℕ) (μ : YoungDiagram) (e : Card d ≃ Cell μ),
         0 < μ.card-μ.rowLen 0 → X ≤ (μ.card:ℝ)/(μ.card-μ.rowLen 0:ℕ) →
         32768000 * Real.log 2 ≤ (1/2:ℝ) * Real.log μ.card →
         ‖sampleOperator (V := hilbertSpace μ) (relabelledUnitary μ e) (palindromePerm d)‖ ≤
   …

   Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.hilbertSpace, OAI.CubeShuffle.palindromePerm

6. theorem OAI.CubeShuffle.UnitaryFinite.medium_exception_decay line 130
7. lemma OAI.CubeShuffle.tail_preserving_pairSwitch line 180
8. lemma OAI.CubeShuffle.pairSwitch_injective line 208
9. def OAI.CubeShuffle.Specht.pairFiberEquiv line 219
10. lemma OAI.CubeShuffle.Specht.pair_sum_taboid_zero line 240
11. lemma OAI.CubeShuffle.Specht.pair_operator_tall_zero line 249
12. lemma OAI.CubeShuffle.Specht.palindrome_tall_zero line 277
13. lemma OAI.CubeShuffle.Specht.palindrome_tall_zero_general line 290
14. theorem OAI.CubeShuffle.Specht.exponential_dimension_spectral line 308

    Source documentation

    Every exponentially large irreducible has the same absolute power decay. Both the high-dimensional FAC.1 and medium-dimensional FAC.2 regimes are used.

    theorem exponential_dimension_spectral (h : ℝ) (hh : 0<h) :
        ∃ a : ℝ, 0<a ∧ ∀ᶠ d : ℕ in atTop, ∀ (μ : YoungDiagram) (e : Card d ≃ Cell μ),
          h*(2:ℝ)^d≤Real.log (Module.finrank ℂ (space μ)) →
          ‖sampleOperator (V := hilbertSpace μ) (relabelledUnitary μ e) (palindromePerm d)‖ ≤
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.space, OAI.CubeShuffle.Specht.hilbertSpace, OAI.CubeShuffle.palindromePerm

15. theorem OAI.CubeShuffle.Specht.spectral_regimes line 382

    Source documentation

    The nontrivial full-deck spectral regimes, with one absolute exponent. The two dimension alternatives are precisely those needed by the shape sum.

    theorem spectral_regimes :
        ∃ a h : ℝ, 0<a ∧ 0<h ∧ ∀ᶠ d : ℕ in atTop,
          ∀ (μ : YoungDiagram) (e : Card d ≃ Cell μ), 0<μ.card-μ.rowLen 0 →
            (μ.colLen 0:ℝ)≤(μ.card:ℝ)/2 →
            ‖sampleOperator (V := hilbertSpace μ) (relabelledUnitary μ e) (palindromePerm d)‖≤
    …

    Mentions: OAI.CubeShuffle.Card, OAI.CubeShuffle.Specht.Cell, OAI.CubeShuffle.Specht.hilbertSpace, OAI.CubeShuffle.palindromePerm