PhysicalOnlineBand.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Online actions from the actual physical child histories

The fixed representative band uses the rational warmup-average child table. Its envelopes scan the literal initial child table. Online gains and decrements are computed from the full physical refinement histories.

theorem OAI.EditApproximation.bandCoordinate_restriction line 19
theorem OAI.EditApproximation.representativeBandActions_wide line 28
theorem OAI.EditApproximation.representativeBandActions_diameter line 41
theorem OAI.EditApproximation.canonicalRoundedBandAction_congr line 58

theorem OAI.EditApproximation.representativeBandActions_canonical_cost line 68

Source documentation

The representative wrapper preserves the literal rounded-band cost bound.

theorem representativeBandActions_canonical_cost {α : Type*} (source target : List α) {M : ℕ}
    (parent : TargetInterval source.length) (r : TargetInterval target.length)
    (thetaExponent b P : ℕ) (tau : ℚ) (htau : 0 < tau)
    (child initial value : Fin M → TargetInterval target.length → ℚ)
    (hnonempty : representativeBandActions source target parent r b P tau
      ((2 : ℚ) ^ (-(thetaExponent : ℤ))) child ≠ [])
    (action : Fin M → TargetInterval target.length)
    (haction : action ∈ representativeBandActions source target parent r b P tau
      ((2 : ℚ) ^ (-(thetaExponent : ℤ))) child)
    (delta L : ℚ) (hL : 0 ≤ L)
    (hspatial : ∀ i s t, value i s ≤ (1 + delta) * value i t + L * targetEndpointDistance s t) :
    let band := representativeBandActions source target parent r b P tau
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.representativeBandActions, OAI.EditApproximation.targetEndpointDistance

def OAI.EditApproximation.physicalBandChildInitial line 117
def OAI.EditApproximation.physicalBandChildMassTable line 120
def OAI.EditApproximation.physicalBandHistory line 123
def OAI.EditApproximation.physicalBandActions line 126
def OAI.EditApproximation.physicalBandEnvelope line 131
theorem OAI.EditApproximation.physicalBandEnvelope_pos line 143
theorem OAI.EditApproximation.physicalBandHistory_nonincreasing line 146
theorem OAI.EditApproximation.physicalBandHistory_bounds line 158
theorem OAI.EditApproximation.physicalBand_coordinate_distance line 171
theorem OAI.EditApproximation.physicalBand_decrement_total line 196
theorem OAI.EditApproximation.physicalBandHistory_absolute line 208
theorem OAI.EditApproximation.physicalBand_decrement_range line 248
theorem OAI.EditApproximation.physicalBand_gain_bounds line 273
def OAI.EditApproximation.physicalBandOnlineDraw line 290
Source documentation
The exact action sampler retains the order of the literal physical band.
```
def physicalBandOnlineDraw (hband : band ≠ []) (η κ : ℚ) (G K t : ℕ)
    (integer : Fin (optimizerTriangularMass K)) : Fin M → TargetInterval target.length :=
…
```
Mentions: OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.TargetInterval
theorem OAI.EditApproximation.physicalBandOnlineDraw_mem line 295
theorem OAI.EditApproximation.physicalBandOnlineDraw_wide line 301
theorem OAI.EditApproximation.physicalBandOnlineDraw_child_cost_mean line 313
Source documentation
Exact conditional mean: only the current finite integer draw is averaged.
```
theorem physicalBandOnlineDraw_child_cost_mean (hband : band ≠ []) (η κ : ℚ)
    (G K t : ℕ) (hK : 0 < K) :
    uniformMean (fun integer : Fin (optimizerTriangularMass K) =>
      let action := physicalBandOnlineDraw source target U N P F A T delta choices node hbelow
…
```
Mentions: OAI.EditApproximation.uniformMean, OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.physicalBandOnlineDraw
theorem OAI.EditApproximation.physicalBandOnlineDraw_computed_mean line 335

theorem OAI.EditApproximation.physicalBand_computed_entropy_regret line 359

Source documentation

The regret hypotheses are proved from the actual physical recurrence.

theorem physicalBand_computed_entropy_regret (htau : 0 < tau) (hdelta : 0 ≤ delta)
    (S H : ℕ) (η κ : ℚ) {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 : ℝ)) ≤ (κ : ℝ)) :
    (∑ t ∈ range S, ∑ coordinate ∈ bandCoordinates (band).toFinset,
        ((childGain mass history t coordinate : ℝ) + childDecrement mass history t coordinate) *
          (actionVector mass comparison coordinate : ℝ)) -
        Real.log (bandCoordinates (band).toFinset).card / (η : ℝ) - 2 * (κ : ℝ) -
          (S : ℝ) / (H : ℝ) ^ 3 ≤
      ∑ t ∈ range S, ∑ coordinate ∈ bandCoordinates (band).toFinset,
        ((childGain mass history t coordinate : ℝ) +
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.bandCoordinates, OAI.EditApproximation.childGain, OAI.EditApproximation.childDecrement, OAI.EditApproximation.actionVector

theorem OAI.EditApproximation.physicalBandOnlineDraw_cost_regret line 396

Source documentation

Expected weighted cost regret of the returned physical-band action.

theorem physicalBandOnlineDraw_cost_regret (htau : 0 < tau) (hdelta : 0 ≤ delta)
    (hband : band ≠ []) (S H G K : ℕ) (η κ : ℚ)
    (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 : ℝ)) ≤ (κ : ℝ)) :
    (∑ t ∈ range S, uniformMean (fun integer : Fin (optimizerTriangularMass K) =>
      let action := physicalBandOnlineDraw source target U N P F A T delta choices node hbelow
…

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

theorem OAI.EditApproximation.physicalBand_canonical_cost line 434

Source documentation

Rounding is charged using the actual spatial regularity of child histories.

theorem physicalBand_canonical_cost (htau : 0 < tau) (hdelta : 0 ≤ delta)
    (hband : band ≠ []) (t : ℕ) (action : Fin M → TargetInterval target.length)
    (haction : action ∈ band) :
    rationalEndpointActionValue r
      (canonicalRoundedBandAction thetaExponent b band hband initial)
      (fun child state => history t (child, state)) ≤
        (1 + delta) * (∑ child, history t (child, action child)) +
          (6 * (128 * F : ℚ) + 2) * theta * ∑ child, mass child := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.rationalEndpointActionValue, OAI.EditApproximation.canonicalRoundedBandAction