OAI/Combinatorics/HadwigerCounterexample/WalshBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.wsign line 12
2. theorem OAI.HadwigerCounterexample.wsign_zero line 14
3. theorem OAI.HadwigerCounterexample.wsign_one line 15
4. theorem OAI.HadwigerCounterexample.wsign_add line 16
5. theorem OAI.HadwigerCounterexample.wsign_abs line 20
6. theorem OAI.HadwigerCounterexample.avg_prod line 24
7. theorem OAI.HadwigerCounterexample.avg_CS line 27
8. theorem OAI.HadwigerCounterexample.wsign_lin line 41

   Source documentation

   Walsh orthogonality via a translation of the uniform measure.

   theorem wsign_lin (b : V →ₗ[F] F) : avg unif (fun x => wsign (b x)) = ind (b=0) := by
   …

   Mentions: OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.avg, OAI.HadwigerCounterexample.unif, OAI.HadwigerCounterexample.wsign, OAI.HadwigerCounterexample.ind

9. theorem OAI.HadwigerCounterexample.wsign_bilin line 58

   Source documentation

   A bilinear signs mean.

   theorem wsign_bilin (b : V →ₗ[F] W →ₗ[F] F) :
       avg (pairW unif unif) (fun x => wsign (b x.1 x.2)) = bp (-(rk b:ℝ)) := by
   …

   Mentions: OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.avg, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.unif, OAI.HadwigerCounterexample.wsign, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.rk

10. theorem OAI.HadwigerCounterexample.avg_ws line 69
11. theorem OAI.HadwigerCounterexample.avg_wsq line 78

    Source documentation

    Unnormalized inner mean square identity.

    theorem avg_wsq (b : V →ₗ[F] W →ₗ[F] F) (v f : Wgt V) :
        avg unif (fun w => (avg v (fun x => f x*wsign (b x w)))^2) =
          avg (pairW v v) (fun x => f x.1 * f x.2 * ind (b x.1=b x.2)) := by
    …

    Mentions: OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.avg, OAI.HadwigerCounterexample.unif, OAI.HadwigerCounterexample.wsign, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.ind

12. theorem OAI.HadwigerCounterexample.bp_half_le line 87
13. theorem OAI.HadwigerCounterexample.walsh_bound line 92

    Source documentation

    Correlation with arbitrary bounded unary tests.

    theorem walsh_bound (b : V →ₗ[F] W →ₗ[F] F) (f : Wgt V) (g : Wgt W)
        (hf : ∀ x, |f x|≤1) (hg : ∀ x, |g x|≤1) :
        |avg unif (fun w => g w * avg unif (fun x => f x*wsign (b x w)))| ≤ bp (-(rk b:ℝ)/2) := by
    …

    Mentions: OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.avg, OAI.HadwigerCounterexample.unif, OAI.HadwigerCounterexample.wsign, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.rk

14. theorem OAI.HadwigerCounterexample.walsh_mass line 131

    Source documentation

    Min-entropy form, squared.

    theorem walsh_mass (b : V →ₗ[F] W →ₗ[F] F) (hb : Function.Injective b) (u : Wgt V) (v : Wgt W)
        (f : Wgt V) (g : Wgt W)
        (hf : ∀ x, |f x|≤1) (hg : ∀ x, |g x|≤1) (hu : SubLaw u) (hv : SubLaw v)
        {p q : ℝ} (hp : ∀ x, u x ≤ p) (hq : ∀ x, v x ≤ q) :
        (avg v (fun w => g w * avg u (fun x => f x*wsign (b x w))))^2 ≤
          (Fintype.card W : ℝ)*p*q := by
    …

    Mentions: OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.SubLaw, OAI.HadwigerCounterexample.avg, OAI.HadwigerCounterexample.wsign