OAI/Analysis/Littlewood/FiniteRank.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.functional_surjective line 16
2. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.nonparallel_pair_surjective line 23
3. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.pair_surjective_or_proportional line 41
4. def OAI.AsymptoticallyMinimalLittlewood.Packing.dotForm line 48
5. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.dotForm_apply line 53
6. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.pair_surjective_of_minor line 56
7. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.exists_nonzero_minor line 77
8. def OAI.AsymptoticallyMinimalLittlewood.Packing.fiber line 98
9. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.mem_fiber line 101
10. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.fiber_card_eq line 105
11. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.fiber_card_mul line 110
12. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.fiber_nonempty line 120
13. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.fiber_le_card line 126
14. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.joint_fiber_eq line 138
15. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.conditional_fiber_card line 144
16. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.conditional_fiber_count line 152
17. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.conditional_card_event line 161
18. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.scalar_preimage_card line 184
19. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.exceptional_centers line 195

    Source documentation

    The exceptional centers have a concrete linear bound in the size of the short-residue set. No joint independence of three or more rows is asserted.

    lemma exceptional_centers {J : Type uJ} [Fintype J] [DecidableEq J]
        (f : J → V →ₗ[K] K) (hpair : ∀ j l, j≠l → Function.Surjective ((f j).prod (f l)))
        (i : J) (hfi : f i≠0) (S : Finset K) :
        ∃ E : Finset K, E.card≤2*(Fintype.card J)^2*S.card ∧
          ∀ s : K, s∉E → ∀ j l, j≠l → ∀ e : Bool,
          Function.Surjective ((f i).prod (if e then f j+f l else f j-f l)) ∨
          ∃ c : K, (if e then f j+f l else f j-f l)=c • f i ∧ c*s∉S := by
    …

20. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.int_cast_ne_zero_of_large_prime line 250
21. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.pair_surjective_integer_minor line 257
22. lemma OAI.AsymptoticallyMinimalLittlewood.Packing.integer_rows_eventual_pair_rank line 267

    Source documentation

    The excluded-prime set is replaced by a concrete size threshold; this suffices because only existence of one sufficiently large prime is needed.

    lemma integer_rows_eventual_pair_rank {ι : Type uι} {J : Type uJ} [Fintype ι] [Fintype J]
        (a : J → ι → ℤ)
        (ha : ∀ j, (fun k ↦ (a j k : ℚ)) ≠ 0)
        (hnp : ∀ j l, j≠l → ∀ c : ℚ,
          (fun k ↦ (a l k : ℚ)) ≠ c • (fun k ↦ (a j k : ℚ))) :
        ∃ Q : ℕ, ∀ q : ℕ, ∀ (_hq : Fact q.Prime), Q<q →
          ∀ j l, j≠l → Function.Surjective
            ((dotForm (fun k ↦ (a j k : ZMod q))).prod
             (dotForm (fun k ↦ (a l k : ZMod q)))) := by
    …

    Mentions: OAI.AsymptoticallyMinimalLittlewood.Packing.dotForm