OAI/Combinatorics/HadwigerCounterexample/SupportedPhaseLaws.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HadwigerCounterexample.Bazaar line 16

   Source documentation

   Tables already fixed on population. bag M is total for convenience but hypotheses on positive mass only apply on the indicated chart.

   structure Bazaar (p : Shape) {N} (n r : ℕ) (T : Cov p N) where
   …

   Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Cov

2. def OAI.HadwigerCounterexample.Bazaar.opened line 24
3. def OAI.HadwigerCounterexample.Bazaar.chart line 28
4. theorem OAI.HadwigerCounterexample.Bazaar.active line 31
5. def OAI.HadwigerCounterexample.Bazaar.pay line 38
6. def OAI.HadwigerCounterexample.loseA line 44
7. def OAI.HadwigerCounterexample.prize line 45
8. def OAI.HadwigerCounterexample.beat line 46
9. def OAI.HadwigerCounterexample.selPrice line 47
10. theorem OAI.HadwigerCounterexample.Bazaar.bag_rate line 53
11. theorem OAI.HadwigerCounterexample.Bazaar.glimpse_prize line 77
12. theorem OAI.HadwigerCounterexample.write_weight line 109
13. theorem OAI.HadwigerCounterexample.mapW_sub line 129
14. theorem OAI.HadwigerCounterexample.walsh_weighted line 139

    Source documentation

    Walsh bound on pushforward tuples with arbitrary separate query weights.

    theorem walsh_weighted (b : V →ₗ[F] V →ₗ[F] F) (hb : Function.Injective b)
        (w : Wgt A) (v : Wgt B) (hw : SubLaw w) (hv : SubLaw v)
        (f : A→V) (g : B→V) (S : Wgt A) (T : Wgt B) {p q : ℝ}
        (hs : ∀ x,|S x|≤1) (ht : ∀ x, |T x| ≤1)
        (hp : ∀ x, mapW w f x ≤ p) (hq : ∀ x,mapW v g x ≤ q) :
        (avg (pairW w v) (fun x => S x.1*T x.2 * wsign (b (f x.1) (g x.2))))^2 ≤ num V*p*q := by
    …

    Mentions: OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.SubLaw, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.avg, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.wsign, OAI.HadwigerCounterexample.num