OAI/Combinatorics/EditApproximation/Geometry/RefinementInitialSupport.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Finite initial-table support for the literal refinement loops. The query value determines the raw local lists; tests of other initial values only remove elements from these lists.

  1. theorem OAI.EditApproximation.refinementInitialSupport_query line 17
  2. theorem OAI.EditApproximation.refinementInitialSupport_local line 21
  3. theorem OAI.EditApproximation.localGroupQueryKeys_congr_initial line 26
  4. theorem OAI.EditApproximation.refinementInitialSupport_cell line 31
  5. theorem OAI.EditApproximation.refinementInitialSupport_online line 44
  6. theorem OAI.EditApproximation.cellRepresentativeStates_congr_initial line 51
  7. theorem OAI.EditApproximation.refinement_local_representatives_congr line 70
  8. theorem OAI.EditApproximation.refinement_cell_representatives_congr line 77
  9. theorem OAI.EditApproximation.queryEarlierRepresentatives_congr_initial line 85
  10. theorem OAI.EditApproximation.queryEarlierInputCover_congr_initial line 97
  11. theorem OAI.EditApproximation.localOnlineCandidates_congr_initial line 119
  12. theorem OAI.EditApproximation.localCellGroupActions_congr_initial line 132
  13. theorem OAI.EditApproximation.querySharedInputCover_congr_initial line 146
  14. theorem OAI.EditApproximation.rationalLocalWideStep_congr_initial line 153
  15. def OAI.EditApproximation.localRefinementInitialQuery line 186

    Source documentation

    First gather the finite parent initial data that select all later representative and cell lists. Child mass/initial data are gathered by a separate layer, independently of the current-index reads.

    def localRefinementInitialQuery : FiniteQuery ι :=
…

    Mentions: OAI.EditApproximation.FiniteQuery

  16. theorem OAI.EditApproximation.localRefinementInitialQuery_value line 193