OAI/Combinatorics/EditApproximation/Geometry/CellGroupSelection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.cellUnskippedBands_length_le line 17
2. theorem OAI.EditApproximation.UnskippedBand.canonicalRounded_congr line 34
3. theorem OAI.EditApproximation.UnskippedBand.rationalAction_wide_mem line 45
4. theorem OAI.EditApproximation.UnskippedBand.rounded_cost line 54
5. theorem OAI.EditApproximation.chooseCellGroupAction_wide_mem line 96
6. theorem OAI.EditApproximation.group_rounding_coefficient line 117
7. theorem OAI.EditApproximation.chooseCellGroup_cone_bound line 128

   Source documentation

   Estimated minimization in an actual whole cell gives the group cone bound simultaneously for every action of the specified member's band.

   theorem chooseCellGroup_cone_bound {α : Type*} (source target : List α) {M : ℕ}
       (parent : TargetInterval source.length) (b P F thetaExponent Q : ℕ) (tau a : ℚ)
       (parentInitial : TargetInterval target.length → ℚ)
       (child initial value : Fin M → TargetInterval target.length → ℚ) (cell : ℕ × ℕ)
       (hnonempty : cellUnskippedBands source target parent b P F thetaExponent tau a
         parentInitial child initial cell ≠ [])
       (draw : ∀ scale : Fin (groupDyadicScales M b F).length,
         Fin (groupSampleCount M Q b (groupDyadicScaleAt M b F scale)) → Fin M)
       (specified : UnskippedBand source target parent b P thetaExponent tau F child initial)
       (hspecified : specified ∈ cellUnskippedBands source target parent b P F thetaExponent tau a
         parentInitial child initial cell)
       (delta L gamma : ℚ) (hF : 1 ≤ F) (hL : 2 ≤ L) (htau : 0 < tau)
   …

   Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.cellUnskippedBands, OAI.EditApproximation.groupDyadicScales, OAI.EditApproximation.groupSampleCount, OAI.EditApproximation.groupDyadicScaleAt, OAI.EditApproximation.UnskippedBand