MonotoneRepresentatives.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem310.ScaleDiscretization.vector_eq_of_sum_eq line 14

Source documentation

On a chain of integer vectors, the sum of the coordinates determines the vector.

lemma vector_eq_of_sum_eq {α : Type u_α} {ι : Type u_ι} [LinearOrder α] [Fintype ι]
    {s : Set α} {f : α → ι → ℤ} (hf : MonotoneOn f s)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s)
    (hs : (∑ i, f x i) = ∑ i, f y i) : f x = f y := by
…

theorem OAI.Problem310.ScaleDiscretization.exists_monotone_representatives line 30

Source documentation

A monotone family of finitely many integer-valued functions has a small common representative set. Unlike a breakpoint construction, this also handles every boundary value without a separate endpoint convention.

theorem exists_monotone_representatives {α : Type u_α} {ι : Type u_ι} [LinearOrder α] [Fintype ι]
    (a b : α) (hab : a ≤ b) (f : α → ι → ℤ)
    (hf : MonotoneOn f (Set.Icc a b)) :
    ∃ R : Finset α,
      (∀ t ∈ R, t ∈ Set.Icc a b) ∧
      R.card ≤ ((∑ i, f b i) + 1 - ∑ i, f a i).toNat ∧
      ∀ t ∈ Set.Icc a b, ∃ t' ∈ R, f t' = f t := by
…

lemma OAI.Problem310.ScaleDiscretization.floor_sub_floor_le_ceil line 66
Source documentation
An integer floor can increase by at most the ceiling of the displacement.
```
lemma floor_sub_floor_le_ceil (x y : ℝ) : ⌊y⌋ - ⌊x⌋ ≤ ⌈y - x⌉ := by
…
```

theorem OAI.Problem310.ScaleDiscretization.exists_affine_floor_representatives line 78

Source documentation

Simultaneous floor keys on an affine path admit at most one plus the sum of their (rounded-up) displacements many representatives.

theorem exists_affine_floor_representatives {ι : Type u_ι} [Fintype ι]
    (a b : ℝ) (hab : a ≤ b) (u v : ι → ℝ) (hv : ∀ i, 0 ≤ v i) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc a b) ∧
      R.card ≤ (1 + ∑ i, ⌈v i * (b - a)⌉).toNat ∧
      ∀ t ∈ Set.Icc a b, ∃ t' ∈ R,
        ∀ i, ⌊u i + v i * t'⌋ = ⌊u i + v i * t⌋ := by
…

theorem OAI.Problem310.ScaleDiscretization.exists_unit_affine_floor_representatives line 108

Source documentation

A uniform displacement bound gives a particularly convenient natural-valued cardinality estimate for the normalized scale interval.

theorem exists_unit_affine_floor_representatives {ι : Type u_ι} [Fintype ι]
    (u v : ι → ℝ) (D : ℕ) (hv : ∀ i, 0 ≤ v i) (hD : ∀ i, v i ≤ (D : ℝ)) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc (1 : ℝ) 2) ∧
      R.card ≤ 1 + Fintype.card ι * D ∧
      ∀ t ∈ Set.Icc (1 : ℝ) 2, ∃ t' ∈ R,
        ∀ i, ⌊u i + v i * t'⌋ = ⌊u i + v i * t⌋ := by
…

lemma OAI.Problem310.ScaleDiscretization.dyadic_grid_slope_le line 131
Source documentation
The padding bound controls the scale-parameter slope of each finest grid key.
```
lemma dyadic_grid_slope_le (B n L : ℕ) (h : B ≤ n + L) :
    (2 : ℝ) ^ B * ((2 : ℝ)⁻¹) ^ n ≤ (2 : ℝ) ^ L := by
…
```

theorem OAI.Problem310.ScaleDiscretization.exists_dyadic_grid_representatives line 140

Source documentation

Simultaneous representatives for the finest dyadic grid keys in a family of local routing tests. Only the padding inequalities are needed.

theorem exists_dyadic_grid_representatives {ι : Type u_ι} [Fintype ι]
    (x : ℝ) (B n : ι → ℕ) (L : ℕ) (hspan : ∀ i, B i ≤ n i + L) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc (1 : ℝ) 2) ∧
      R.card ≤ 1 + Fintype.card ι * 2 ^ L ∧
      ∀ t ∈ Set.Icc (1 : ℝ) 2, ∃ t' ∈ R,
        ∀ i, ⌊(2 : ℝ) ^ B i * (x + t' * ((2 : ℝ)⁻¹) ^ n i)⌋ =
          ⌊(2 : ℝ) ^ B i * (x + t * ((2 : ℝ)⁻¹) ^ n i)⌋ := by
…

lemma OAI.Problem310.ScaleDiscretization.periodic_floor_eq_of_floor_eq line 163

Source documentation

Passing from a real-line dyadic cell to its periodic key loses no information.

lemma periodic_floor_eq_of_floor_eq (q : ℕ) {y z : ℝ}
    (h : ⌊(2 : ℝ) ^ q * y⌋ = ⌊(2 : ℝ) ^ q * z⌋) :
    ⌊(2 : ℝ) ^ q * Int.fract y⌋ = ⌊(2 : ℝ) ^ q * Int.fract z⌋ := by
…

theorem OAI.Problem310.ScaleDiscretization.exists_periodic_dyadic_representatives line 182

Source documentation

Periodic versions of all finest keys agree at one of the same representatives.

theorem exists_periodic_dyadic_representatives {ι : Type u_ι} [Fintype ι]
    (x : ℝ) (B n : ι → ℕ) (L : ℕ) (hspan : ∀ i, B i ≤ n i + L) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc (1 : ℝ) 2) ∧
      R.card ≤ 1 + Fintype.card ι * 2 ^ L ∧
      ∀ t ∈ Set.Icc (1 : ℝ) 2, ∃ t' ∈ R,
        ∀ i, ⌊(2 : ℝ) ^ B i * Int.fract (x + t' * ((2 : ℝ)⁻¹) ^ n i)⌋ =
          ⌊(2 : ℝ) ^ B i * Int.fract (x + t * ((2 : ℝ)⁻¹) ^ n i)⌋ := by
…

theorem OAI.Problem310.ScaleDiscretization.exists_local_predicate_representatives line 199

Source documentation

Deterministic representatives simultaneously work for every assignment of local predicates that factors through the indicated periodic keys. In particular the representatives do not depend on the random selector or terminal tables.

theorem exists_local_predicate_representatives {ι : Type u_ι} [Fintype ι]
    (x : ℝ) (B n : ι → ℕ) (L : ℕ) (hspan : ∀ i, B i ≤ n i + L) :
    ∃ R : Finset ℝ,
      (∀ t ∈ R, t ∈ Set.Icc (1 : ℝ) 2) ∧
      R.card ≤ 1 + Fintype.card ι * 2 ^ L ∧
      ∀ t ∈ Set.Icc (1 : ℝ) 2, ∃ t' ∈ R,
        ∀ Q : ι → ℝ → Bool,
          (∀ i y z, ⌊(2 : ℝ) ^ B i * Int.fract y⌋ =
            ⌊(2 : ℝ) ^ B i * Int.fract z⌋ → Q i y = Q i z) →
          ∀ i, Q i (x + t' * ((2 : ℝ)⁻¹) ^ n i) =
            Q i (x + t * ((2 : ℝ)⁻¹) ^ n i) := by
…

lemma OAI.Problem310.ScaleDiscretization.representative_card_budget line 217
Source documentation
The stronger monotone-key estimate is within the entropy budget.
```
lemma representative_card_budget (M r D : ℕ) (hM : 1 ≤ M) (hr : 1 ≤ r) :
    1 + (M - 1) * r * D ≤ 20 * M * r * (1 + D) := by
…
```