PhysicalExpectedRegret.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Conditional prefix regret from the exact physical-band sampler.

theorem OAI.EditApproximation.uniformMean_sub line 12
theorem OAI.EditApproximation.sampledPrefixRegret_child_identity line 16

theorem OAI.EditApproximation.physicalBand_prefix_expected_regret line 50

Source documentation

Every deterministic prefix uses the same actual computed online mixtures. Clipping comparison children only decreases the prefix regret.

theorem physicalBand_prefix_expected_regret (htau : 0 < tau) (hdelta : 0 ≤ delta)
    (hband : band ≠ []) (C S H G K : ℕ) (hCS : C ≤ S) (η κ : ℚ)
    (hG : G = H + (bandCoordinates (band).toFinset).card + 2) (hK : K = G ^ 80)
    (comparison : Fin M → TargetInterval target.length) (hc : comparison ∈ band)
    (hH : 4 ≤ H) (hη : 0 < η) (hκ : 0 ≤ κ) (hκhalf : κ ≤ 1 / 2)
    (hηrange : (η : ℝ) *
      (2 * (delta : ℝ) + 8 * ((128 * F : ℚ) : ℝ) * (theta : ℝ)) ≤ (κ : ℝ)) (charge : ℝ) :
    (∑ t ∈ range C, uniformMean (fun integer : Fin (optimizerTriangularMass K) =>
      sampledPrefixRegret charge (κ : ℝ) (fun t coordinate => (history t coordinate : ℝ))
        (physicalComparisonClipped source target U N P F A T delta choices node hbelow comparison)
        (fun j => physicalBandOnlineDraw source target U N P F A T delta choices node hbelow
          b thetaExponent tau r hband η κ G K j integer) t)) ≤
…

Mentions: OAI.EditApproximation.bandCoordinates, OAI.EditApproximation.TargetInterval, OAI.EditApproximation.uniformMean, OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.sampledPrefixRegret, OAI.EditApproximation.physicalComparisonClipped, OAI.EditApproximation.physicalBandOnlineDraw

theorem OAI.EditApproximation.unskippedGroupFailure_true line 90

theorem OAI.EditApproximation.physicalNode_groupFailure_probability line 102

Source documentation

Per-scale finite Bernstein bounds imply the whole-cell failure probability.

theorem physicalNode_groupFailure_probability {α : Type*} [DecidableEq α]
    (source target : List α) (N : ℕ) (hN : 0 < N) (hell : 1764 ≤ inputSmallLog N)
    {M J P F b Q thetaExponent : ℕ} [NeZero M]
    [MeasurableSpace (Fin M)] [MeasurableSingletonClass (Fin M)]
    (hM : 0 < M) (hMeq : M = (integerParameters N).M)
    (hPeq : P = (integerParameters N).P) (hFeq : F = inputSmallLog N)
    (eb : ℕ) (hbeq : b = 2 ^ eb) (hQeq : Q = inputSmallLog N ^ 80)
    (hthetaeq : thetaExponent = 40 * smallLogExponent N)
    (U : PhysicalEntry M J target.length → ℕ) (A : ℚ)
    (hsize : source.length + target.length ≤ N) (hP : 66 ≤ P) (hA : 1 ≤ A)
    (hseed : ∀ state, stateEditCost (physicalSource source state.1) target state.2 ≤ U state ∧
      (U state : ℚ) ≤ A * stateEditCost (physicalSource source state.1) target state.2)
…

Mentions: OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.integerParameters, OAI.EditApproximation.smallLogExponent, OAI.EditApproximation.PhysicalEntry, OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource