OAI/Combinatorics/EditApproximation/Numerics/RationalWideStep.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.rationalMinimum_map_mono line 14
2. theorem OAI.EditApproximation.rationalBellman_mono line 23
3. theorem OAI.EditApproximation.rationalBellman_le_action line 32
4. theorem OAI.EditApproximation.rationalOnlineMinimum_lower line 41
5. def OAI.EditApproximation.rationalWideStepCone line 52
6. def OAI.EditApproximation.rationalWideStep line 62
7. theorem OAI.EditApproximation.rationalWideStep_bellman_sandwich line 73

   Source documentation

   Both lower candidates are genuine current-child wide Bellman cones. The sampled choices enter only through literal membership in the wide list.

   theorem rationalWideStep_bellman_sandwich {nx ny M : ℕ} (parent : TargetInterval nx)
       (representatives : List (ℕ × TargetInterval ny)) (P : ℕ)
       (initial : TargetInterval ny → ℚ) (L delta : ℚ)
       (old current : Fin M × TargetInterval ny → ℚ) (hmono : current ≤ old)
       (groups online : List (RationalBellmanAction (TargetInterval ny) (Fin M × TargetInterval ny) M))
       (hgroups : ∀ action ∈ groups, action ∈ rationalActualWideActions parent representatives P)
       (honline : ∀ action ∈ online, action ∈ rationalActualWideActions parent representatives P)
       (q : TargetInterval ny) :
       rationalBellman initial (fun q r => targetEndpointDistance q r) L
           (rationalActualWideActions parent representatives P) current q ≤
         rationalWideStep parent representatives P initial L delta old current groups online q ∧
       rationalWideStep parent representatives P initial L delta old current groups online q ≤
   …

   Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.RationalBellmanAction, OAI.EditApproximation.rationalActualWideActions, OAI.EditApproximation.rationalBellman, OAI.EditApproximation.targetEndpointDistance, OAI.EditApproximation.rationalWideStep