WeightedRank.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.positions_le line 18
lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.layer_card line 26

theorem OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape.Weights.weighted_rank_bound line 35

Source documentation

Source weighted-coincidence for literal field positions and the SAME good arrays that were selected with all conditional tests.

theorem weighted_rank_bound {M n K : ℕ} {α β δ : ℝ} {w : Entry (SymmetricAlphabet n) → Bool}
    (h : GoodUpTo M α β δ w) (hs : s ≤ M) (hu : u ≤ M) (hq : q ≤ M) (hv : v ≤ M)
    (σ : T.Pos v → SymmetricAlphabet n) (hi : Function.Injective (T.row σ))
    (hp : BernoulliCandidates.Present T.row w σ)
    (htK : ∀ a, W.top a ≤ K) (hfK : ∀ b, W.fan b ≤ K)
    (hqK : ∀ e, W.square e ≤ K) (hdK : ∀ e, W.six e ≤ K) :
    ((∑ j ∈ Finset.range K, Coincidence.rankOn (fun p => (σ p).1)
      (Finset.univ.filter (fun p => j < W.position p)) : ℕ) : ℝ) ≤
      ((3-β)-7*(2-α)) * (∑ a, (W.top a : ℝ)) + (2-α) * (∑ b, (W.fan b : ℝ)) +
        (2-δ) * (∑ e, (W.square e : ℝ)) + (3-δ) * (∑ e, (W.six e : ℝ)) := 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.contact_bound line 55

Source documentation

Literal internal-letter-contact estimate. The hypotheses on contacts are exactly the indexed-side normality and side multiplicity conditions supplied by source normal form; arbitrary cycles of contacts are allowed.

theorem contact_bound {M n K : ℕ} {α β δ : ℝ} {w : Entry (SymmetricAlphabet n) → Bool}
    (h : GoodUpTo M α β δ w) (hs : s ≤ M) (hu : u ≤ M) (hq : q ≤ M) (hv : v ≤ M)
    (σ : T.Pos v → SymmetricAlphabet n) (hi : Function.Injective (T.row σ))
    (hp : BernoulliCandidates.Present T.row w σ)
    (htK : ∀ a, W.top a ≤ K) (hfK : ∀ b, W.fan b ≤ K)
    (hqK : ∀ e, W.square e ≤ K) (hdK : ∀ e, W.six e ≤ K)
    {E : Type*} [Fintype E] [DecidableEq E] (l r : E → T.Pos v)
    (hne : ∀ e, l e ≠ r e) (hc : ∀ e, (σ (l e)).1 = (σ (r e)).1)
    (hcap : ∀ p, (Finset.univ.filter (fun e => l e = p ∨ r e = p)).card ≤ W.position p) :
    (Fintype.card E : ℝ) ≤ ((3-β)-7*(2-α)) * (∑ a, (W.top a : ℝ)) +
      (2-α) * (∑ b, (W.fan b : ℝ)) + (2-δ) * (∑ e, (W.square e : ℝ)) +
      (3-δ) * (∑ e, (W.six e : ℝ)) := by
…