WeightRounding.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Finite codes for downward rounding of grouped weights

For a positive mesh δ, a weight in [0, 1] is rounded down to δ * floor (w / δ). Its integer coefficient is an actual element of Fin (floor (1 / δ) + 1), including the possible endpoint w = 1. The error estimates apply to every indicator with values in [0, 1].

def OAI.MetricEntropyDuality.weightCodeSize line 30
Source documentation
The number of possible rounded values of a weight in [0, 1].
```
def weightCodeSize (δ : ℝ) : ℕ := Nat.floor (1 / δ) + 1
```
theorem OAI.MetricEntropyDuality.weightCodeSize_pos line 32
def OAI.MetricEntropyDuality.roundWeight line 36
Source documentation
Downward rounding to the mesh δ.
```
def roundWeight (δ w : ℝ) : ℝ := δ * (Nat.floor (w / δ) : ℝ)
```
def OAI.MetricEntropyDuality.decodeWeight line 39
Source documentation
Decode an integer weight code using the fixed mesh.
```
def decodeWeight (δ : ℝ) (c : Fin (weightCodeSize δ)) : ℝ := δ * (c.val : ℝ)
```
Mentions: OAI.MetricEntropyDuality.weightCodeSize
def OAI.MetricEntropyDuality.weightCode line 43
Source documentation
The integer coefficient of every rounded weight is within the finite code range. The positivity and interval hypotheses are explicit.
```
def weightCode (δ w : ℝ) (hδ : 0 < δ) (_hw0 : 0 ≤ w) (hw1 : w ≤ 1) :
    Fin (weightCodeSize δ) :=
…
```
Mentions: OAI.MetricEntropyDuality.weightCodeSize
theorem OAI.MetricEntropyDuality.weightCode_val line 48
theorem OAI.MetricEntropyDuality.decodeWeight_weightCode line 52
theorem OAI.MetricEntropyDuality.roundWeight_zero line 56
theorem OAI.MetricEntropyDuality.roundWeight_nonneg line 59
theorem OAI.MetricEntropyDuality.roundWeight_le line 62
theorem OAI.MetricEntropyDuality.roundWeight_sub_lt line 69
Source documentation
The downward rounding error is strictly smaller than one mesh interval.
```
theorem roundWeight_sub_lt {δ w : ℝ} (hδ : 0 < δ) :
    w - roundWeight δ w < δ := by
…
```
Mentions: OAI.MetricEntropyDuality.roundWeight
theorem OAI.MetricEntropyDuality.roundWeight_error line 76
theorem OAI.MetricEntropyDuality.weightCodeSize_le line 82
Source documentation
The finite integer code count satisfies the real-valued bound used in the compression estimate.
```
theorem weightCodeSize_le {δ : ℝ} (hδ : 0 < δ) :
    (weightCodeSize δ : ℝ) ≤ 1 + 1 / δ := by
…
```
Mentions: OAI.MetricEntropyDuality.weightCodeSize

theorem OAI.MetricEntropyDuality.roundWeight_mul_error line 89

Source documentation

Multiplying by a number in [0, 1] cannot increase the rounding loss.

theorem roundWeight_mul_error {δ w b : ℝ} (hδ : 0 < δ) (hw0 : 0 ≤ w)
    (hb0 : 0 ≤ b) (hb1 : b ≤ 1) :
    0 ≤ w * b - roundWeight δ w * b ∧
      w * b - roundWeight δ w * b ≤ δ := by
…

Mentions: OAI.MetricEntropyDuality.roundWeight

theorem OAI.MetricEntropyDuality.roundWeight_sum_error line 100

Source documentation

Simultaneous rounding of an actual finite array of weights loses at most one mesh interval for each array entry.

theorem roundWeight_sum_error {I : Type uI} [Fintype I]
    (δ : ℝ) (hδ : 0 < δ) (w b : I → ℝ)
    (hw0 : ∀ i, 0 ≤ w i) (hb0 : ∀ i, 0 ≤ b i) (hb1 : ∀ i, b i ≤ 1) :
    0 ≤ (∑ i, w i * b i) - ∑ i, roundWeight δ (w i) * b i ∧
      (∑ i, w i * b i) - ∑ i, roundWeight δ (w i) * b i ≤
        (Fintype.card I : ℝ) * δ := by
…

Mentions: OAI.MetricEntropyDuality.roundWeight

def OAI.MetricEntropyDuality.roundingStep line 120
Source documentation
The mesh used for one level of the partition compression.
```
def roundingStep (θ : ℝ) (s u : ℕ) : ℝ := θ / ((s : ℝ) * 2 ^ u)
```
theorem OAI.MetricEntropyDuality.roundingStep_pos line 122
theorem OAI.MetricEntropyDuality.slotTag_card line 126
theorem OAI.MetricEntropyDuality.card_mul_roundingStep line 132
Source documentation
The actual number of slot/subset pairs times the mesh equals the prescribed per-level error.
```
theorem card_mul_roundingStep (θ : ℝ) {s u : ℕ} (hs : 0 < s) :
    (Fintype.card (Fin s × Finset (Fin u)) : ℝ) * roundingStep θ s u = θ := by
…
```
Mentions: OAI.MetricEntropyDuality.roundingStep
theorem OAI.MetricEntropyDuality.weightCodeSize_roundingStep line 140
Source documentation
The finite code size counts all integers from zero through floor (s * 2^u / θ), inclusive.
```
theorem weightCodeSize_roundingStep (θ : ℝ) (s u : ℕ) :
    weightCodeSize (roundingStep θ s u) =
      Nat.floor (((s : ℝ) * 2 ^ u) / θ) + 1 := by
…
```
Mentions: OAI.MetricEntropyDuality.weightCodeSize, OAI.MetricEntropyDuality.roundingStep

theorem OAI.MetricEntropyDuality.roundWeight_level_error line 147

Source documentation

The total loss at a single level is at most θ, for the exact index type Fin s × Finset (Fin u) used by the finite compression codes.

theorem roundWeight_level_error {θ : ℝ} {s u : ℕ} (hθ : 0 < θ) (hs : 0 < s)
    (w b : Fin s → Finset (Fin u) → ℝ)
    (hw0 : ∀ k T, 0 ≤ w k T) (hb0 : ∀ k T, 0 ≤ b k T)
    (hb1 : ∀ k T, b k T ≤ 1) :
    0 ≤ (∑ k, ∑ T, w k T * b k T) -
        ∑ k, ∑ T, roundWeight (roundingStep θ s u) (w k T) * b k T ∧
      (∑ k, ∑ T, w k T * b k T) -
        ∑ k, ∑ T, roundWeight (roundingStep θ s u) (w k T) * b k T ≤ θ := by
…

Mentions: OAI.MetricEntropyDuality.roundWeight, OAI.MetricEntropyDuality.roundingStep