OAI/Analysis/FreeWords/ProjectionSmall.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeLiftFrontier.IsDiffuse line 15
  2. theorem OAI.KKProjectionSupport.trace_projection_nonneg line 45
  3. theorem OAI.KKProjectionSupport.trace_projection_pos line 50
  4. theorem OAI.KKProjectionSupport.projection_half line 57
  5. theorem OAI.KKProjectionSupport.projection_trace_dyadic line 72
  6. theorem OAI.KKProjectionSupport.exists_small_projection line 87