Oracle-relative Kolmogorov complexity -- proof internals #
theorem
Complexity.OracleTM.plainKolmogorovComplexity_le_internal
{n : ℕ}
{machine : OracleTM n}
{oracle : BooleanOracle}
{program output : List Bool}
(hproduce : machine.Produces oracle program output)
:
theorem
Complexity.OracleTM.timeBoundedKolmogorovComplexity_le_internal
{n : ℕ}
{machine : OracleTM n}
{oracle : BooleanOracle}
{program output : List Bool}
{time : ℕ}
(hproduce : machine.ProducesInTime oracle program output time)
:
theorem
Complexity.OracleTM.timeBoundedKolmogorovComplexity_eq_top_iff_internal
{n : ℕ}
(machine : OracleTM n)
(oracle : BooleanOracle)
(output : List Bool)
(time : ℕ)
:
machine.timeBoundedKolmogorovComplexity oracle output time = ⊤ ↔ ¬∃ (program : List Bool), machine.ProducesInTime oracle program output time
theorem
Complexity.OracleTM.timeBoundedKolmogorovComplexity_witness_internal
{n : ℕ}
(machine : OracleTM n)
(oracle : BooleanOracle)
(output : List Bool)
(time : ℕ)
(hfinite : machine.timeBoundedKolmogorovComplexity oracle output time ≠ ⊤)
:
∃ (program : List Bool),
↑program.length = machine.timeBoundedKolmogorovComplexity oracle output time ∧ machine.ProducesInTime oracle program output time
theorem
Complexity.OracleTM.timeBoundedKolmogorovComplexity_le_coe_iff_internal
{n : ℕ}
(machine : OracleTM n)
(oracle : BooleanOracle)
(output : List Bool)
(time bound : ℕ)
:
machine.timeBoundedKolmogorovComplexity oracle output time ≤ ↑bound ↔ ∃ (program : List Bool), program.length ≤ bound ∧ machine.ProducesInTime oracle program output time
theorem
Complexity.OracleTM.timeBoundedKolmogorovComplexity_mono_internal
{n : ℕ}
(machine : OracleTM n)
(oracle : BooleanOracle)
(output : List Bool)
{first second : ℕ}
(hclock : first ≤ second)
:
machine.timeBoundedKolmogorovComplexity oracle output second ≤ machine.timeBoundedKolmogorovComplexity oracle output first
theorem
Complexity.OracleTM.polynomialTimeOverhead_kolmogorov_transfer_internal
{simulatorTapes sourceTapes : ℕ}
{simulator : OracleTM simulatorTapes}
{source : OracleTM sourceTapes}
{compile : List Bool → List Bool}
{constant : ℕ}
{clock : TM.TimeOverhead}
(hsim : simulator.SimulatesInTime source compile clock)
(hlength : TM.HasAdditiveProgramOverhead compile constant)
(hclock : TM.PolynomialTimeOverhead clock)
:
∃ (coefficient : ℕ) (exponent : ℕ),
∀ (oracle : BooleanOracle) (output : List Bool) (sourceTime bound : ℕ),
source.timeBoundedKolmogorovComplexity oracle output sourceTime ≤ ↑bound →
simulator.timeBoundedKolmogorovComplexity oracle output (coefficient * (bound + sourceTime + 1) ^ exponent) ≤ ↑(bound + constant)
theorem
Complexity.TM.toOracleTM_timeBoundedKolmogorovComplexity_eq_internal
{n : ℕ}
(machine : TM n)
(oracle : BooleanOracle)
(output : List Bool)
(time : ℕ)
:
machine.toOracleTM.timeBoundedKolmogorovComplexity oracle output time = machine.timeBoundedKolmogorovComplexity output time