OAI/Combinatorics/BooleanFunctions/Projection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SquareRootDegree.Projection.conditional_eq_of_projection line 17

   Source documentation

   Conditional averages are characterized by their cell moments.

   theorem conditional_eq_of_projection (F : α → β) (g h : α → ℝ)
       (hp : ∀ p : β → ℝ, average (fun x => p (F x)*g x) = average (fun x => p (F x)*h x)) :
       conditionalAverage F g = conditionalAverage F h := by
   …

   Mentions: OAI.SquareRootDegree.average, OAI.SquareRootDegree.conditionalAverage

2. theorem OAI.SquareRootDegree.Projection.conditional_nested line 26
3. theorem OAI.SquareRootDegree.Projection.pi_projection line 33
4. theorem OAI.SquareRootDegree.Projection.pi_conditional_sum line 50
5. theorem OAI.SquareRootDegree.Projection.conditional_equiv line 64
6. theorem OAI.SquareRootDegree.Projection.cellMass_pos line 83
7. theorem OAI.SquareRootDegree.Projection.conditional_const_mul line 93
8. theorem OAI.SquareRootDegree.Projection.conditional_comp line 102
9. theorem OAI.SquareRootDegree.Projection.conditional_add line 115
10. theorem OAI.SquareRootDegree.Projection.conditional_tuple_sum line 125