LocalWeightedRank.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.rank_level_bound_local line 20

Source documentation

Only the occurrence collections retained at each positive weight level need be small; the complete alphabet's array is not bounded by the fragment. This is the literal layer application of source diagram:weighted-rank.

theorem rank_level_bound_local {M n : ℕ} {α β δ : ℝ} {w : Entry (SymmetricAlphabet n) → Bool}
    (h : GoodUpTo M α β δ w) (j : ℕ)
    (hs : Fintype.card (W.TopAt j) ≤ M) (hu : Fintype.card (W.FanAt j) ≤ M)
    (hq : Fintype.card (W.SquareAt j) ≤ M) (hv : Fintype.card (W.SixAt j) ≤ M)
    (σ : T.Pos v → SymmetricAlphabet n) (hi : Function.Injective (T.row σ))
    (hp : BernoulliCandidates.Present T.row w σ) :
    (Coincidence.rankOn (fun p => (σ p).1) (Finset.univ.filter (fun p => j < W.position p)) : ℝ) ≤
      ((3-β)-7*(2-α)) * Fintype.card (W.TopAt j) + (2-α) * Fintype.card (W.FanAt j) +
        (2-δ) * Fintype.card (W.SquareAt j) + (3-δ) * Fintype.card (W.SixAt j) := by
…

Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Entry, OAI.HyperbolicObstruction.IncidenceTemplate.SymmetricAlphabet, OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.GoodUpTo, OAI.HyperbolicObstruction.BernoulliCandidates.Present, OAI.HyperbolicObstruction.Coincidence.rankOn

theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.weighted_rank_bound_local line 38
theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.contact_bound_local line 57