Documentation

LeanPool.ParameterFreeGradient.V7.Proofs.Stage1E03.Certificate

Correctness certificates for all possible reports of the Euclidean local trial.

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

Classical proposition decisions used locally by the trace certificate.

Equations
Instances For
    source
    theorem V7.Stage1E03.sourcePlannedTrace_exact {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (M : ℝ) (n : ℕ) :
    TraceExact inst.oracle (sourcePlannedTrace inst M n)
    source
    theorem V7.Stage1E03.fullShape_trace_exact {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (report : TrialReport d) (hshape : FullReportShape inst eps M n report) :
    TraceExact inst.oracle report.trace
    source
    theorem V7.Stage1E03.fullShape_guard_data {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (cached : CachedPair d) (hcached : cached.observation = O3.PairOracle.observe inst.oracle x0) (report : TrialReport d) (hshape : FullReportShape inst eps M n report) :
    GuardDataExact cached inst.oracle report
    source
    theorem V7.Stage1E03.fullShape_outcome_exhaustive {d : ℕ} (report : TrialReport d) :
    TrialOutcomeExhaustive report
    source
    theorem V7.Stage1E03.fullShape_scale_lt {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (heps : 0 < eps) (hM : 0 < M) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (report : TrialReport d) (hshape : FullReportShape inst eps M n report) (failed : ObservableGuardCheck d) (hout : report.outcome = TrialOutcome.scale failed) :
    M < inst.L
    source
    theorem V7.Stage1E03.holds_imply_not_fails {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (cached : CachedPair d) (hcached : cached.observation = O3.PairOracle.observe inst.oracle x0) (report : TrialReport d) (hshape : FullReportShape inst eps M n report) (hall : ∀ check ∈ report.checkedGuards, CheckHolds 2 M check) (check : ObservableGuardCheck d) :
    check ∈ report.checkedGuards → ¬GuardFails 2 M inst.oracle check.failure
    source
    theorem V7.Stage1E03.source_phaseA_accepted {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M D : ℝ) (n : ℕ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (report : TrialReport d) (hall : ∀ check ∈ report.checkedGuards, CheckHolds 2 M check) (hguards : report.checkedGuards = sourceGuardSchedule inst M n) :
    O3.EuclideanEstimateAccepted (legacyInstance inst eps heps hG) M n
    source
    theorem V7.Stage1E03.source_interpolation_accepted {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (heps : 0 < eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (report : TrialReport d) (hall : ∀ check ∈ report.checkedGuards, CheckHolds 2 M check) (hguards : report.checkedGuards = sourceGuardSchedule inst M n) :
    O3.OGMGAllInterpolationGuardsHold (O3.stage9ExecutionConfig n (legacyInstance inst eps heps hG).oracle M (O3.euclideanEstimateState (legacyInstance inst eps heps hG) M n).accelerated)
    source
    theorem V7.Stage1E03.source_terminal_accepted {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M : ℝ) (n : ℕ) (heps : 0 < eps) (hM : 0 < M) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (report : TrialReport d) (hall : ∀ check ∈ report.checkedGuards, CheckHolds 2 M check) (hguards : report.checkedGuards = sourceGuardSchedule inst M n) :
    (O3.ogmgTerminalDescentCheck (O3.stage9ExecutionConfig n (legacyInstance inst eps heps hG).oracle M (O3.euclideanEstimateState (legacyInstance inst eps heps hG) M n).accelerated)).Holds
    source
    theorem V7.Stage1E03.fullShape_radius_lt {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M D : ℝ) (n : ℕ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (hn : 1 ≤ n) (hnEq : n = horizon eps M D) (hkappa : 1 ≤ M * D / eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (report : TrialReport d) (hshape : FullReportShape inst eps M n report) (terminal : Observation d) (hout : report.outcome = TrialOutcome.radius terminal) :
    D < inst.R
    source
    theorem V7.Stage1E03.source_trial_certificate {d : ℕ} {x0 : Point d} (inst : PositiveInstance 2 d x0) (eps M D : ℝ) (n : ℕ) (heps : 0 < eps) (hM : 0 < M) (hD : 0 < D) (hn : 1 ≤ n) (hnEq : n = horizon eps M D) (hkappa : 1 ≤ M * D / eps) (hG : eps < lpNorm 2 (inst.oracle.gradient x0)) (cached : CachedPair d) (hcached : cached.observation = O3.PairOracle.observe inst.oracle x0) (report : TrialReport d) (hshape : FullReportShape inst eps M n report) :
    TrialCertificate eps 2 M D inst.L inst.R cached inst.oracle report