OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternSumCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.sum_injective_assignments line 10
2. theorem OAI.Ostmann.sum_external_injective_pattern line 17
3. theorem OAI.Ostmann.sum_external_injective_pattern_fin line 34

   Source documentation

   This is an exact zero extension of the original injective class sum; it is the form to which the independent-prior comparison applies.

   theorem sum_external_injective_pattern_fin {A B C M : Type*}
       [Fintype A] [Fintype B] [Fintype C] [AddCommMonoid M] {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (F : (B → A) → (C → A) → M) :
       (∑ y : B → A, ∑ z : {z : C → A // Function.Injective z}, F y z.val) =
         ∑ x : Fin (N + 1) → A,
           if Function.Injective (fun c => x (e.symm (.inr c))) then
             F (fun b => x (e.symm (.inl b))) (fun c => x (e.symm (.inr c))) else 0 := by
   …