Building the conditional difference estimator from one ordinary estimator #
-- proof internals
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.SupportsPairUpper.pair_upper_internal
{ordinaryTapes conditionalTapes : ℕ}
{plan : Plan}
{composition : PairCompositionPlan}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
(hsupports : SupportsPairUpper plan composition ordinaryMachine conditionalMachine)
(inst : MINCKT.Instance)
:
ordinaryMachine.timeBoundedKolmogorovComplexity (pair inst.output inst.condition) (plan.pairInputTime inst) ≤ inst.complexity conditionalMachine + ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time + ↑(plan.pairUpperLoss inst)
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Compatible.satisfiesSoIInputsOnQueries_internal
{ordinaryTapes conditionalTapes : ℕ}
{plan : Plan}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{ordinaryParameters : GapMINKT.Logarithmic.Parameters}
{conditionalParameters : Parameters}
{soiClock soiLoss : ℕ → ℕ}
(hcompatible :
Compatible plan ordinaryMachine conditionalMachine ordinaryParameters conditionalParameters soiClock soiLoss)
{estimate : GapMINKT.Logarithmic.Estimator}
(hestimate : estimate.SatisfiesBoundsOn ordinaryMachine ordinaryParameters plan.IsEstimatorQuery)
:
(plan.components estimate).SatisfiesSoIInputs (plan.accountingSchedule ordinaryParameters) ordinaryMachine
conditionalMachine conditionalParameters soiClock soiLoss
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Compatible.satisfiesSoIInputs_internal
{ordinaryTapes conditionalTapes : ℕ}
{plan : Plan}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{ordinaryParameters : GapMINKT.Logarithmic.Parameters}
{conditionalParameters : Parameters}
{soiClock soiLoss : ℕ → ℕ}
(hcompatible :
Compatible plan ordinaryMachine conditionalMachine ordinaryParameters conditionalParameters soiClock soiLoss)
{estimate : GapMINKT.Logarithmic.Estimator}
(hestimate : estimate.SatisfiesBounds ordinaryMachine ordinaryParameters)
:
(plan.components estimate).SatisfiesSoIInputs (plan.accountingSchedule ordinaryParameters) ordinaryMachine
conditionalMachine conditionalParameters soiClock soiLoss