Shape.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Pos line 18
Source documentation
Literal field positions in source diagram:rank.
```
abbrev Pos (v : ℕ) := Fin s ⊕ ((Σ b : Fin u, rowSupport (.inl (T.1 b))) ⊕
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.rowSupport
abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Trial line 21
def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.coreCoord line 23
def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.topCoord line 33

def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.row line 40

Source documentation

Every position refers to the original arrays. A top is its independent mark, not a new independent copy of its correlated fan entries.

def row {A : Type*} (σ : T.Pos v → A) : Trial s u q v → Entry A
  | .inl a => .inl ⟨.inr (.inl ()),fun f => σ (T.topCoord a f)⟩
  | .inr (.inl b) => .inl ⟨.inl (T.1 b),fun f => σ (.inr (.inl ⟨b,f⟩))⟩
  | .inr (.inr (.inl e)) => .inl ⟨.inr (.inr (T.2.2 e)),fun f => σ (.inr (.inr (.inl ⟨e,f⟩)))⟩
  | .inr (.inr (.inr e)) => .inr (fun i => σ (.inr (.inr (.inr (e,i)))))

Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Trial, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Entry

def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.cost line 46
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.probability_row line 52
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.square_card line 57
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.cardinal_positions line 60
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.rank_budget line 69
Source documentation
Cancellation of the field count with the exact negative Bernoulli costs. This is the source rank budget, with p=3-beta and f=2-alpha.
```
lemma rank_budget (α β δ : ℝ) : (Fintype.card (T.Pos v):ℝ) + ∑ r : Trial s u q v, T.cost α β δ r =
    ((3-β)-7*(2-α))*s + (2-α)*u + (2-δ)*q + (3-δ)*v := by
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Trial
def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Good line 80
Source documentation
The source good-rank condition for this literal collection shape.
```
def Good {n : ℕ} (α β δ : ℝ) (w : Entry (SymmetricAlphabet n) → Bool) : Prop :=
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet
instance OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.(instance at line 86) line 86
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.not_good_iff line 89
theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.bad_bound line 97
Source documentation
Source diagram:rank for a fixed shape, uniformly over all literal signed assignments and all distinct actual trials.
```
theorem bad_bound {n : ℕ} {α β δ : ℝ}
    (ha : 0 ≤ α) (hb : 7*α ≤ β) (hd : 0 ≤ δ) :
    (FiniteLaw.bernoulliProduct (probability α β δ (SymmetricAlphabet n))
      (probability_mem ha hb hd)).prob (fun w => ¬T.Good (v := v) α β δ w) ≤
…
```
Mentions: OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.probability, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.probability_mem