TrialAddresses.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem310.TrialAddresses.GridAddress line 15
Source documentation
Coordinates of a finite family of dyadic tables. Different table names are different coordinates even when their numeric cell keys coincide.
```
abbrev GridAddress {E : Type u_E} (b : E → ℕ) := Σ e : E, Fin (2 ^ (b e + 2))
```
def OAI.Problem310.TrialAddresses.centerAddress line 17
theorem OAI.Problem310.TrialAddresses.centerAddress_injective line 20
theorem OAI.Problem310.TrialAddresses.dyadicKey_eq_of_refine line 26
Source documentation
Refinement preserves all equalities needed to recover a coarse key.
```
theorem dyadicKey_eq_of_refine {b B : ℕ} {x y : ℝ} (hb : b ≤ B)
    (h : dyadicKey B x = dyadicKey B y) : dyadicKey b x = dyadicKey b y := by
…
```
def OAI.Problem310.TrialAddresses.trialAddress line 31

theorem OAI.Problem310.TrialAddresses.trialAddress_ne_center line 36

Source documentation

A tested coordinate is distinct from every center-exposed coordinate.

theorem trialAddress_ne_center {I : Type u_I} {E : Type u_E} (b : E → ℕ) (edge : I → E)
    (n : I → ℕ) (x t : ℝ) (htlo : 1 ≤ t) (hthi : t ≤ 2)
    (hnlo : ∀ i, 3 ≤ n i) (hnhi : ∀ i, n i ≤ b (edge i)) (i : I) (e : E) :
    trialAddress b edge n x t i ≠ centerAddress b x e := by
…

Mentions: OAI.Problem310.TrialAddresses.trialAddress, OAI.Problem310.TrialAddresses.centerAddress

theorem OAI.Problem310.TrialAddresses.trialAddress_disjoint_center line 50

Source documentation

The entire fresh trial-coordinate set is disjoint from the full center exposure, including tables outside the center's actual route.

theorem trialAddress_disjoint_center {I : Type u_I} {E : Type u_E} (b : E → ℕ) (edge : I → E)
    (n : I → ℕ) (x t : ℝ) (htlo : 1 ≤ t) (hthi : t ≤ 2)
    (hnlo : ∀ i, 3 ≤ n i) (hnhi : ∀ i, n i ≤ b (edge i)) :
    Disjoint (Set.range (trialAddress b edge n x t))
      (Set.range (centerAddress b x)) := by
…

Mentions: OAI.Problem310.TrialAddresses.trialAddress, OAI.Problem310.TrialAddresses.centerAddress

theorem OAI.Problem310.TrialAddresses.trialAddress_injective line 60

Source documentation

Distinct table/index pairs give distinct fresh selector coordinates.

theorem trialAddress_injective {I : Type u_I} {E : Type u_E} (b : E → ℕ) (edge : I → E)
    (n : I → ℕ) (x t : ℝ) (htlo : 1 ≤ t) (hthi : t ≤ 2)
    (hnlo : ∀ i, 3 ≤ n i) (hnhi : ∀ i, n i ≤ b (edge i))
    (hpair : Function.Injective (fun i => (edge i, n i))) :
    Function.Injective (trialAddress b edge n x t) := by
…

Mentions: OAI.Problem310.TrialAddresses.trialAddress

theorem OAI.Problem310.TrialAddresses.terminalAddress_injective line 82

Source documentation

Adaptive terminal addresses are injective whenever equal leaves force the same child subtree, and each terminal resolution refines that child's incoming grid. The leaf selection may otherwise depend arbitrarily on all selector tables.

theorem terminalAddress_injective {I : Type u_I} {C : Type u_C} {L : Type u_L}
    (child : I → C) (n : I → ℕ) (leaf : I → L)
    (b : C → ℕ) (B : L → ℕ) (x t : ℝ)
    (htlo : 1 ≤ t) (hthi : t ≤ 2)
    (hnlo : ∀ i, 3 ≤ n i) (hnhi : ∀ i, n i ≤ b (child i))
    (hrefine : ∀ i, b (child i) ≤ B (leaf i))
    (hbranch : ∀ i j, leaf i = leaf j → child i = child j)
    (hpair : Function.Injective (fun i => (child i, n i))) :
    Function.Injective (trialAddress B leaf n x t) := by
…

Mentions: OAI.Problem310.TrialAddresses.trialAddress

abbrev OAI.Problem310.TrialAddresses.WindowTrial line 108
Source documentation
A uniform block of r indices for each of M nondefault children. This finite trial type has exactly the exponent used in the miss formula.
```
abbrev WindowTrial (M r : ℕ) := Fin M × Fin r
```
def OAI.Problem310.TrialAddresses.windowTrialIndex line 110
theorem OAI.Problem310.TrialAddresses.card_windowTrial line 113
theorem OAI.Problem310.TrialAddresses.windowTrialIndex_bounds line 116
theorem OAI.Problem310.TrialAddresses.windowTrial_pair_injective line 124