OAI/Combinatorics/EditApproximation/Refinement/PhysicalRefinementInvariants.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.stageWarmup_at_terminal line 9
2. theorem OAI.EditApproximation.physicalRefinement_at_terminal line 26
3. theorem OAI.EditApproximation.physicalRefinement_zero line 41
4. theorem OAI.EditApproximation.stageWarmup_postfixed line 58
5. theorem OAI.EditApproximation.physicalRefinement_bellman_invariants line 75

   Source documentation

   The full recurrence is postfixed for the current-child Bellman operator, and each next value is at most the previous-child Bellman value. Selected actions require only their literal wide-list membership certificates.

   theorem physicalRefinement_bellman_invariants {α : Type*} [DecidableEq α] {M J : ℕ}
       (source target : List α) (U : PhysicalEntry M J target.length → ℕ)
       (N P F : ℕ) (A : ℚ) (T : ℕ) (delta : ℚ)
       (choices : PhysicalSelections M J source.length target.length P
         (stageRepresentatives source target U N P F A)) (node : PhysicalNode M J) :
       let value := fun t (s : PhysicalEntry M J target.length) =>
   …

   Mentions: OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.PhysicalSelections, OAI.EditApproximation.stageRepresentatives, OAI.EditApproximation.PhysicalNode

6. theorem OAI.EditApproximation.physicalRefinement_nonincreasing line 134
7. theorem OAI.EditApproximation.physicalRefinement_le_warmup line 145
8. theorem OAI.EditApproximation.physicalRefinement_lower line 159

   Source documentation

   Lower invariants propagate down the physical tree from the initial table bounds.

   theorem physicalRefinement_lower {α : Type*} [DecidableEq α] {M J : ℕ}
       (source target : List α) (hM : 0 < M) (U : PhysicalEntry M J target.length → ℕ)
       (N P F : ℕ) (A : ℚ) (T : ℕ) (delta : ℚ) (a : ℝ) (ha : 1 ≤ a)
       (hL : (1 : ℝ) ≤ ((128 * F : ℚ) : ℝ))
       (hinit : physicalLower source target a ≤ fun s => (stageInitial source target U N P F A s : ℝ))
       (choices : PhysicalSelections M J source.length target.length P
         (stageRepresentatives source target U N P F A)) (node : PhysicalNode M J)
       (t : ℕ) (q : TargetInterval target.length) :
       physicalLower source target a (node, q) ≤
         (physicalRefinement source target U N P F A T delta choices node t q : ℝ) := by
   …

   Mentions: OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.physicalLower, OAI.EditApproximation.stageInitial, OAI.EditApproximation.PhysicalSelections, OAI.EditApproximation.stageRepresentatives, OAI.EditApproximation.PhysicalNode, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.physicalRefinement

9. theorem OAI.EditApproximation.physicalRefinement_stage_bounds line 204