OAI/Combinatorics/EditApproximation/Geometry/RefinementDataQuery.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Adaptive gathering of all fixed data used by one local refinement entry: parent initial values, child warmup masses and child initial values. Only the raw local support and the resulting wide coordinate lists are requested. The later earlier/current gathers remain those of the literal local refinement query.

  1. def OAI.EditApproximation.localRefinementBandDataQuery line 25
  2. theorem OAI.EditApproximation.localRefinementBandDataQuery_value line 33
  3. def OAI.EditApproximation.localRefinementDataQuery line 86
  4. theorem OAI.EditApproximation.localRefinementDataQuery_value line 93