OAI/Analysis/PlaneSpectrum/Selections.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanFiveColor.GeneralPosition.spanning_selection line 11

    Source documentation

    A cover evaluated at a large general-position set contains a spanning monochromatic subset.

    lemma spanning_selection {ι : Type*} (Q : Finset ι) (S : Finset V) (hS : General S)
    (hcard : Q.card*(finrank ℚ V-1) < S.card)
    (A : ι → V → Prop) (hA : ∀ x ∈ S, ∃ i ∈ Q, A i x) :
    ∃ i ∈ Q, ∃ T ⊆ S, T.card = finrank ℚ V ∧
      Submodule.span ℚ (T : Set V) = ⊤ ∧ ∀ x ∈ T, A i x := by
…

    Mentions: OAI.EuclideanFiveColor.GeneralPosition.General

  2. lemma OAI.EuclideanFiveColor.Arithmetic.common_denominator line 43
  3. lemma OAI.EuclideanFiveColor.Arithmetic.uniform_integral_representations line 54
  4. lemma OAI.EuclideanFiveColor.Arithmetic.span_mult_rep line 101
  5. lemma OAI.EuclideanFiveColor.Arithmetic.uniform_selection line 114

    Source documentation

    Uniform integral spanning selections extracted from the source's syndetic cover.

    lemma uniform_selection (Q : Finset ℂ)
    (hQn : ∀ q ∈ Q, ‖q‖ = 1) (hQa : ∀ q ∈ Q, IsAlgebraic ℚ q)
    (A : ℂ → Prop)
    (hA : ∀ v : ℂ, ‖v‖ = 1 → IsAlgebraic ℚ v → ∃ q ∈ Q, A (q*v)) :
    ∃ D M : ℕ, 0 < D ∧ 0 < M ∧ ∀ v : ℂ, ‖v‖ = 1 → IsAlgebraic ℚ v →
      ∃ n : ℕ, ∃ k : Fin n → ℂ, ∃ a b : Fin n → ℤ,
        (∀ j, ‖k j‖ = 1 ∧ IsAlgebraic ℚ (k j) ∧ A (k j*v)) ∧
        (∑ j, a j • k j) = D • (1:ℂ) ∧
        (∑ j, b j • k j) = D • Complex.I ∧
        (∑ j, ((a j).natAbs+(b j).natAbs)) ≤ M := by
…
  6. lemma OAI.EuclideanFiveColor.Arithmetic.real_sum_bound line 181
  7. lemma OAI.EuclideanFiveColor.Arithmetic.selection_transverse line 195
  8. def OAI.EuclideanFiveColor.CappedResidues.Good line 250
  9. lemma OAI.EuclideanFiveColor.CappedResidues.good_mono line 253
  10. lemma OAI.EuclideanFiveColor.CappedResidues.good_zero line 257
  11. lemma OAI.EuclideanFiveColor.CappedResidues.good_diff line 263
  12. lemma OAI.EuclideanFiveColor.CappedResidues.add_residues line 271
  13. lemma OAI.EuclideanFiveColor.CappedResidues.input_residue line 299
  14. lemma OAI.EuclideanFiveColor.CappedResidues.list_residue line 318
  15. lemma OAI.EuclideanFiveColor.CappedResidues.list_cap line 334
  16. def OAI.EuclideanFiveColor.CappedResidues.signedList line 362
  17. lemma OAI.EuclideanFiveColor.CappedResidues.signedList_length line 367
  18. lemma OAI.EuclideanFiveColor.CappedResidues.signedList_sum line 370
  19. lemma OAI.EuclideanFiveColor.CappedResidues.signedList_mem line 374
  20. lemma OAI.EuclideanFiveColor.CappedResidues.integer_list line 380
  21. lemma OAI.EuclideanFiveColor.CappedResidues.integer_cap line 402
  22. lemma OAI.EuclideanFiveColor.CappedResidues.integer_abs_cap line 414