OAI/Combinatorics/EditApproximation/Geometry/Bellman.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Finite Bellman propagation and warmup

The action minimum is computed by a finite list with the initial cone as fallback. Empty action families need no extended-real convention. The warmup lemmas concern the actual repeated finite Bellman operator.

  1. def OAI.EditApproximation.finiteMinimum line 17
  2. theorem OAI.EditApproximation.le_finiteMinimum_iff line 21
  3. theorem OAI.EditApproximation.finiteMinimum_le_fallback line 28
  4. theorem OAI.EditApproximation.finiteMinimum_le_member line 34
  5. theorem OAI.EditApproximation.finiteMinimum_map_mono line 43
  6. theorem OAI.EditApproximation.finiteMinimum_map_add line 54
  7. theorem OAI.EditApproximation.finiteMinimum_map_spatial line 62
  8. structure OAI.EditApproximation.BellmanAction line 71
  9. def OAI.EditApproximation.bellmanActionValue line 76
  10. def OAI.EditApproximation.finiteBellman line 81
  11. theorem OAI.EditApproximation.finiteBellman_le_fallback line 86
  12. theorem OAI.EditApproximation.finiteBellman_mono line 92
  13. theorem OAI.EditApproximation.finiteBellman_le_action line 103
  14. theorem OAI.EditApproximation.finiteBellman_lower line 111
  15. theorem OAI.EditApproximation.finiteBellman_spatial line 124
  16. def OAI.EditApproximation.warmup line 138
  17. def OAI.EditApproximation.finiteBellmanSystem line 145

    Source documentation

    A finite system of node-specific action lists. Child states may belong to any lower level of the source tree.

    def finiteBellmanSystem {State : Type*} {M : ℕ}
    (initial : State → ℝ) (distance : State → State → ℝ) (L : ℝ)
    (actions : State → List (BellmanAction State State M))
    (child : State → ℝ) (query : State) : ℝ :=
…

    Mentions: OAI.EditApproximation.BellmanAction

  18. theorem OAI.EditApproximation.finiteBellmanSystem_monotone line 151
  19. theorem OAI.EditApproximation.finiteBellmanSystem_le_initial line 158
  20. theorem OAI.EditApproximation.warmup_nonincreasing line 165
  21. theorem OAI.EditApproximation.warmup_lower line 174
  22. theorem OAI.EditApproximation.finite_bellman_warmup_nonincreasing line 184
  23. def OAI.EditApproximation.warmupAverage line 192
  24. theorem OAI.EditApproximation.warmup_average_sandwich line 197
  25. theorem OAI.EditApproximation.warmup_average_action_bound line 217

    Source documentation

    Averaging the actual one-step action inequality gives the warmup mass slack, with the exact endpoint correction before its simplification to the nonnegative initial-cone charge.

    theorem warmup_average_action_bound {State ι : Type*} [Fintype ι]
    (operator : (State → ℝ) → State → ℝ) (initial : State → ℝ)
    (T : ℕ) (hT : 0 < T) (parent : State) (child : ι → State) (charge : ℝ)
    (haction : ∀ t < T, warmup operator initial (t + 1) parent ≤
      charge + ∑ i, warmup operator initial t (child i)) :
    warmupAverage operator initial T parent -
        (initial parent - warmup operator initial T parent) / T ≤
      charge + ∑ i, warmupAverage operator initial T (child i) := by
…

    Mentions: OAI.EditApproximation.warmup, OAI.EditApproximation.warmupAverage