OAI/Combinatorics/UniformKServer/FlowAuxiliary.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Linear adapted auxiliary potentials commute with posterior filtering.

  1. def OAI.UniformKServer.PilotEdits.linearPotential line 14
  2. theorem OAI.UniformKServer.PilotEdits.linear_filtering line 16
  3. theorem OAI.UniformKServer.PilotEdits.linear_bounds line 36
  4. theorem OAI.UniformKServer.PilotEdits.linear_edits line 45