BandActionGuards.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Actual rounded band actions pass the finite guards

Each child uses its own envelope-derived integer spacing. The action is rounded with literal integer division; wide-grid, radius and imbalance claims are proved for these returned states.

theorem OAI.EditApproximation.bandChildEnvelope_pos line 23
theorem OAI.EditApproximation.roundedBandAction_endpoint_error line 30
theorem OAI.EditApproximation.roundedBandAction_distance line 42

theorem OAI.EditApproximation.roundedBandAction_guards line 56

Source documentation

Actual rounded wide membership and imbalance guard. The sum premise is supplied by bandChildEnvelope_sum_guard, and the remaining premises are explicit computed-parameter inequalities.

theorem roundedBandAction_guards {α : Type*} (source target : List α)
    {M b P : ℕ} (parent : TargetInterval source.length) (r : TargetInterval target.length)
    (thetaExponent : ℕ) (tau velocity : ℚ)
    (child initial : Fin M → TargetInterval target.length → ℚ)
    (action : Fin M → TargetInterval target.length)
    (haction : action ∈ computedBandActions parent r b P tau ((2 : ℚ) ^ (-(thetaExponent : ℤ))) velocity child)
    (hM : 0 < M) (hPpos : 0 < P)
    (hbPower : ∃ e : ℕ, b = 2 ^ e) (hPPower : ∃ e : ℕ, P = 2 ^ e)
    (hscale : (M : ℚ) ≤ (2 : ℚ) ^ (-(thetaExponent : ℤ)) * P)
    (F : ℚ)
    (hsmall : 64 * F * (2 : ℚ) ^ (-(thetaExponent : ℤ)) ≤ 4)
    (htheta : (2 : ℚ) ^ (-(thetaExponent : ℤ)) ≤ 1 / 2)
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.computedBandActions

theorem OAI.EditApproximation.connectionBudget_pair_perturbation line 132

Source documentation

Moving the two endpoints of each interval charges at most their total movement, including the outside connections.

theorem connectionBudget_pair_perturbation {n : ℕ}
    (pairs : List (TargetInterval n × TargetInterval n)) (beforeStart afterStart finish : ℕ) :
    connectionBudget afterStart (pairs.map Prod.snd) finish ≤
      connectionBudget beforeStart (pairs.map Prod.fst) finish + Nat.dist afterStart beforeStart +
        (pairs.map fun pair => targetEndpointDistance pair.1 pair.2).sum := by
…

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

theorem OAI.EditApproximation.endpointActionConnection_perturbation line 151

theorem OAI.EditApproximation.roundedBandAction_connection line 162

Source documentation

The returned rounded action pays at most 2 θ ∑ hᵢ in actual connection cost when its unrounded band action has zero connection.

theorem roundedBandAction_connection {n M : ℕ} (r : TargetInterval n)
    (thetaExponent b : ℕ) (band : List (Fin M → TargetInterval n))
    (initial : Fin M → TargetInterval n → ℚ) (action : Fin M → TargetInterval n)
    (hzero : endpointActionConnection r action = 0) :
    (endpointActionConnection r (roundedBandAction thetaExponent b band initial action) : ℚ) ≤
      2 * (2 : ℚ) ^ (-(thetaExponent : ℤ)) * ∑ i, bandChildEnvelope b band initial i := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.endpointActionConnection, OAI.EditApproximation.roundedBandAction, OAI.EditApproximation.bandChildEnvelope

theorem OAI.EditApproximation.canonicalRoundedBandAction_connection line 183

theorem OAI.EditApproximation.roundedBandAction_initialValue line 200

Source documentation

The initial table's literal spatial bound controls the value of every returned rounded state.

theorem roundedBandAction_initialValue {ny M : ℕ} (thetaExponent b : ℕ)
    (band : List (Fin M → TargetInterval ny))
    (initial : Fin M → TargetInterval ny → ℚ) (action : Fin M → TargetInterval ny)
    (L0 : ℚ) (hL0 : 0 ≤ L0)
    (hspatial : ∀ i s t, initial i s ≤ initial i t + L0 * targetEndpointDistance s t)
    (i : Fin M) :
    initial i (roundedBandAction thetaExponent b band initial action i) ≤ initial i (action i) +
      2 * L0 * (2 : ℚ) ^ (-(thetaExponent : ℤ)) * bandChildEnvelope b band initial i := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.targetEndpointDistance, OAI.EditApproximation.roundedBandAction, OAI.EditApproximation.bandChildEnvelope

theorem OAI.EditApproximation.roundedBandAction_initialValue_le_twice line 219

theorem OAI.EditApproximation.canonicalRoundedBandAction_distance line 235

Source documentation

The canonical rounded action is close to every member of its actual computed band, with distance measured at both child endpoints.

theorem canonicalRoundedBandAction_distance {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (thetaExponent b P : ℕ) (tau velocity : ℚ) (htau : 0 < tau)
    (child initial : Fin M → TargetInterval ny → ℚ)
    (hnonempty : computedBandActions parent r b P tau
      ((2 : ℚ) ^ (-(thetaExponent : ℤ))) velocity child ≠ [])
    (action : Fin M → TargetInterval ny)
    (haction : action ∈ computedBandActions parent r b P tau
      ((2 : ℚ) ^ (-(thetaExponent : ℤ))) velocity child) (i : Fin M) :
    let band := computedBandActions parent r b P tau
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.computedBandActions

theorem OAI.EditApproximation.canonicalRoundedBandAction_cost line 283

Source documentation

The actual canonical rounded action satisfies the rounded-action cost inequality uniformly for every actual band member.

theorem canonicalRoundedBandAction_cost {nx ny M : ℕ} (parent : TargetInterval nx)
    (r : TargetInterval ny) (thetaExponent b P : ℕ) (tau velocity : ℚ) (htau : 0 < tau)
    (child initial value : Fin M → TargetInterval ny → ℚ)
    (hnonempty : computedBandActions parent r b P tau
      ((2 : ℚ) ^ (-(thetaExponent : ℤ))) velocity child ≠ [])
    (action : Fin M → TargetInterval ny)
    (haction : action ∈ computedBandActions parent r b P tau
      ((2 : ℚ) ^ (-(thetaExponent : ℤ))) velocity child)
    (delta L : ℚ) (hL : 0 ≤ L)
    (hspatial : ∀ i s t, value i s ≤ (1 + delta) * value i t + L * targetEndpointDistance s t) :
    let band := computedBandActions parent r b P tau
…

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