OAI/Analysis/Cotype/CubeFirstChaos.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Cotype.walshVector line 12
  2. theorem OAI.Cotype.vectorWalsh_inversion line 15
  3. theorem OAI.Cotype.walshVector_inversion line 37
  4. theorem OAI.Cotype.coordinateExpectation_walshVector line 43
  5. theorem OAI.Cotype.coordinate_firstCoefficient_eq_radProjection line 54
  6. theorem OAI.Cotype.coordinate_firstCoefficient_probabilityL2_norm line 78