BandRounding.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Integer rounding spacings from the dyadic band envelopes

Taking the nonnegative part of the dyadic product exponent computes the integer spacing max(1, theta*h). The resulting spacing preserves the wide grid by actual divisibility of powers of two.

theorem OAI.EditApproximation.dyadic_nonnegative_spacing line 23
theorem OAI.EditApproximation.bandRoundSpacing_exact line 36
theorem OAI.EditApproximation.bandRoundSpacing_pos line 47
theorem OAI.EditApproximation.gridRound_scaled_error line 56
Source documentation
Actual division rounding moves each endpoint by at most the scaled child envelope, including the special spacing-one case.
```
theorem gridRound_scaled_error (spacing position : ℕ) (scaled : ℚ)
    (hspacing : (spacing : ℚ) = max 1 scaled) (hscaled : 0 ≤ scaled) :
    (Nat.dist position (gridRound spacing position) : ℚ) ≤ scaled := by
…
```
Mentions: OAI.EditApproximation.gridRound
theorem OAI.EditApproximation.dyadic_dvd_of_le line 77
theorem OAI.EditApproximation.seedGridSpacing_dyadic line 84

theorem OAI.EditApproximation.bandRoundSpacing_wide_grid line 98

Source documentation

The envelope floor and the numerical theta*P ≥ M ensure that the actual rounded integer spacing is a multiple of the actual wide grid.

theorem bandRoundSpacing_wide_grid {ny M b P : ℕ} (thetaExponent : ℕ)
    (band : List (Fin M → TargetInterval ny))
    (initial : Fin M → TargetInterval ny → ℚ) (i : Fin M)
    (hM : 0 < M) (hPpos : 0 < P)
    (hbPower : ∃ e : ℕ, b = 2 ^ e) (hPPower : ∃ e : ℕ, P = 2 ^ e)
    (hscale : (M : ℚ) ≤ (2 : ℚ) ^ (-(thetaExponent : ℤ)) * P) :
    seedGridSpacing b P ∣ bandRoundSpacing thetaExponent b band initial i := by
…

Mentions: OAI.EditApproximation.TargetInterval, OAI.EditApproximation.seedGridSpacing, OAI.EditApproximation.bandRoundSpacing