OAI/Combinatorics/HadwigerCounterexample/FiniteAffineLaws.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.card_space line 18
2. theorem OAI.HadwigerCounterexample.add_polar line 25
3. theorem OAI.HadwigerCounterexample.translate_cap line 30

   Source documentation

   Equally likely images along every direction of an indexed family. The translation hypothesis is before testing the specified targets.

   theorem translate_cap [Fintype V] [Fintype W] {T : Type*} [Fintype T] [Nonempty T]
       {w : Wgt V} (hw : SubLaw w)
       (f : V →ₗ[F] W) (g : T ↪ W) (h : ∀ t, ∃ v, f v = g t ∧ ∀ x, w (x+v) = w x) (y : W) :
       pr w (fun x => f x=y) ≤ (Fintype.card T : ℝ)⁻¹ := by
   …

   Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.SubLaw, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.pr

4. theorem OAI.HadwigerCounterexample.unif_lin line 59
5. theorem OAI.HadwigerCounterexample.pr_unif_lin line 75
6. theorem OAI.HadwigerCounterexample.map_unif_surjective line 82
7. theorem OAI.HadwigerCounterexample.dim_mat line 89