OAI/NumberTheory/Ostmann/Construction/MatchedCellSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Disjoint prime cells force every nonzero matching to preserve its cell

  1. theorem OAI.Ostmann.matched_prior_preserves_cell line 10
  2. theorem OAI.Ostmann.matched_prior_zero_of_changes_cell line 25
  3. theorem OAI.Ostmann.matched_correlation_zero_of_changes_cell line 37
  4. theorem OAI.Ostmann.matched_prior_preserves_prime_label line 50

    Source documentation

    The same conclusion uses the actual prime-cell labeling directly.

    theorem matched_prior_preserves_prime_label {H K : Type*} [Fintype H]
    (P : Finset ℕ) (Q : H → Finset ℕ) (label : H → K) (cell : ℕ → K)
    (hsupport : ∀ i p, p ∈ Q i → cell p = label i)
    (e : Equiv.Perm H) (x : H → P)
    (hx : (∏ i, primeSubsetPrior P (Q i) (x i)) ≠ 0)
    (he : (∏ i, primeSubsetPrior P (Q i) (x (e i))) ≠ 0) :
    ∀ i, label (e i) = label i := by
…

    Mentions: OAI.Ostmann.primeSubsetPrior

  5. theorem OAI.Ostmann.matched_correlation_zero_of_changes_prime_label line 63