RankSampling.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.eventually_exists_tables line 18
theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.eventually_exists_tables_precision line 46
Source documentation
Arbitrary finite conditional sampling data and the literal bounded-rank producer are simultaneous on arbitrarily large original signed alphabets.
```
theorem eventually_exists_tables_precision {J : Type*} [Fintype J]
    (T : J → ConditionalTest) (M : ℕ) {α β δ ξ τ : ℝ}
    (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ) (hd1 : δ < 1)
    (hsmall : ∀ j, ((T j).k+1:ℝ)*(β+90*δ) ≤ 1/2)
    (hξ : 0 < ξ) (hτ0 : 0 < τ) (hτ2 : τ ≤ 2) :
    ∀ᶠ n in atTop, ∃ (w : TableModel.Entry (A := SymmetricAlphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.ConditionalTest, OAI.HyperbolicObstruction.TableModel.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport
structure OAI.HyperbolicObstruction.IncidenceTemplate.RankSamplingStage line 81
Source documentation
A genuine stage with a bounded-rank certificate for the same arrays. The size cutoff is arbitrary and fixed before the alphabet is selected.
```
structure RankSamplingStage (m M : ℕ) (φ : ℝ) extends SamplingStage m φ where
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage
lemma OAI.HyperbolicObstruction.IncidenceTemplate.exists_rankSamplingStage line 84
def OAI.HyperbolicObstruction.IncidenceTemplate.actualRankSamplingStage line 108
Source documentation
Diagonalizing in the desired diagram size imposes no additional sampling hypothesis, and does not change the defining presentation.
```
def actualRankSamplingStage (M : ℕ → ℕ) (m : ℕ) : RankSamplingStage m (M m) (samplingParameter m) :=
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.RankSamplingStage, OAI.HyperbolicObstruction.IncidenceTemplate.samplingParameter
def OAI.HyperbolicObstruction.IncidenceTemplate.rankSelectedStage line 112
lemma OAI.HyperbolicObstruction.IncidenceTemplate.rankSelectedStage_good line 115