Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Semantics

Compatibility of source Euclidean states and recorded checks with the original analytic execution.

source
@[instance_reducible]
noncomputable def V7.Stage1E03.semanticsPropDecidable (q : Prop) :
Decidable q

Classical proposition decisions used locally in the source semantics proof.

Equations
Instances For
    source
    theorem V7.Stage1E03.minimizer_gradient_zero {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) {xstar : Point d} (hxstar : xstar ∈ MinimizerSet inst.oracle) :
    inst.oracle.gradient xstar = 0
    source
    noncomputable def V7.Stage1E03.legacyInstance {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
    O3.AdmissibleInstance d 2

    The current positive instance expressed in the original admissible-instance interface.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem V7.Stage1E03.legacyInstance_oracle {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
      (legacyInstance inst eps heps hG).oracle = inst.oracle
      source
      @[simp]
      theorem V7.Stage1E03.legacyInstance_L {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
      (legacyInstance inst eps heps hG).L = inst.L
      source
      @[simp]
      theorem V7.Stage1E03.legacyInstance_f {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
      (legacyInstance inst eps heps hG).f = inst.oracle.value
      source
      @[simp]
      theorem V7.Stage1E03.legacyInstance_grad {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
      (legacyInstance inst eps heps hG).grad = inst.oracle.gradient
      source
      @[simp]
      theorem V7.Stage1E03.legacyInstance_eps {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
      (legacyInstance inst eps heps hG).eps = eps
      source
      @[simp]
      theorem V7.Stage1E03.legacyInstance_x0 {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
      (legacyInstance inst eps heps hG).x0 = x0
      source
      @[simp]
      theorem V7.Stage1E03.legacyInstance_radius {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) :
      (legacyInstance inst eps heps hG).radius = inst.R
      source
      theorem V7.Stage1E03.sourceEstimateState_eq_legacy {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (k : ℕ) :
      sourceEstimateState inst.oracle M x0 k = O3.euclideanEstimateState (legacyInstance inst eps heps hG) M k
      source
      theorem V7.Stage1E03.sourceU_eq_legacy {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (n : ℕ) :
      sourceU inst M n = (O3.euclideanEstimateState (legacyInstance inst eps heps hG) M n).accelerated
      source
      theorem V7.Stage1E03.check_eq_exact_of_observations {d : ℕ} (oracle : PairOracle d) (check : ObservableGuardCheck d) (hx : check.xPair = O3.PairOracle.observe oracle check.xPair.point) (hy : check.yPair = O3.PairOracle.observe oracle check.yPair.point) :
      check = exactGuardCheck check.kind oracle check.xPair.point check.yPair.point
      source
      theorem V7.Stage1E03.not_guardFails_of_checkHolds {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (check : ObservableGuardCheck d) (hx : check.xPair = O3.PairOracle.observe oracle check.xPair.point) (hy : check.yPair = O3.PairOracle.observe oracle check.yPair.point) (hcheck : CheckHolds p M check) :
      ¬GuardFails p M oracle check.failure
      source
      theorem V7.Stage1E03.guardFails_of_not_checkHolds {d : ℕ} (p M : ℝ) (oracle : PairOracle d) (check : ObservableGuardCheck d) (hx : check.xPair = O3.PairOracle.observe oracle check.xPair.point) (hy : check.yPair = O3.PairOracle.observe oracle check.yPair.point) (hcheck : ¬CheckHolds p M check) :
      GuardFails p M oracle check.failure