Feasibility and invariant domain of the v5 local policy

theorem FD1D.V5.LocalPolicy.discrepancy_le_half_iff_regularizedMass_le {a p h : ℝ} {x y : ℕ} (ha : 0 < a) : discrepancy a p h x y ≤ h / 2 ↔ regularizedMass a p x y ≤ h

theorem FD1D.V5.LocalPolicy.parent_interval_bound {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (ht : discrepancy a p h x y ≤ h / 2) : p ≤ h * (inventory x y + a / 2)

theorem FD1D.V5.LocalPolicy.orderedBias_nonneg {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) (hxy : y ≤ x) (ht : discrepancy a p h x y ≤ h / 2) : 0 ≤ orderedBias a p h x y

theorem FD1D.V5.LocalPolicy.bias_nonneg_of_ordered {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hh : 0 < h) (hxy : y ≤ x) (ht : discrepancy a p h x y ≤ h / 2) : 0 ≤ bias a p h x y

theorem FD1D.V5.LocalPolicy.orderedBias_le_uniform {a p h : ℝ} {x y : ℕ} (hxy : y ≤ x) (hy : 0 < y) : orderedBias a p h x y ≤ uniformCandidate h x y

theorem FD1D.V5.LocalPolicy.orderedBias_lt_parentMass_of_pos {a p h : ℝ} {x y : ℕ} (hh : 0 < h) (hxy : y ≤ x) (hy : 0 < y) : orderedBias a p h x y < parentMass h x y

theorem FD1D.V5.LocalPolicy.massLeft_eq_count_mul_rateLeft (a p h : ℝ) (x y : ℕ) : massLeft a p h x y = ↑x * rateLeft a p h x y

theorem FD1D.V5.LocalPolicy.massRight_eq_count_mul_rateRight (a p h : ℝ) (x y : ℕ) : massRight a p h x y = ↑y * rateRight a p h x y

theorem FD1D.V5.LocalPolicy.child_invariants {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hp : 0 < p) (hh : 0 < h) (ht : discrepancy a p h x y ≤ h / 2) : discrepancyLeft a p h x y ≤ rateLeft a p h x y / 2 ∧ regularizedMassLeft a p x ≤ rateLeft a p h x y ∧ discrepancyRight a p h x y ≤ rateRight a p h x y / 2 ∧ regularizedMassRight a p y ≤ rateRight a p h x y

theorem FD1D.V5.LocalPolicy.child_rates_nonneg {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hp : 0 < p) (hh : 0 < h) (ht : discrepancy a p h x y ≤ h / 2) : 0 ≤ rateLeft a p h x y ∧ 0 ≤ rateRight a p h x y

theorem FD1D.V5.LocalPolicy.child_rate_average_ge {a p h : ℝ} {x y : ℕ} (ht : discrepancy a p h x y ≤ h / 2) : h ≤ (rateLeft a p h x y + rateRight a p h x y) / 2

theorem FD1D.V5.LocalPolicy.child_rate_energy_ge {a p h : ℝ} {x y : ℕ} (ha : 0 < a) (hp : 0 < p) (hh : 0 < h) (ht : discrepancy a p h x y ≤ h / 2) : h ^ 2 ≤ (rateLeft a p h x y ^ 2 + rateRight a p h x y ^ 2) / 2