StarActual.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.StarModel.sum_array_le line 20
lemma OAI.HyperbolicObstruction.IncidenceTemplate.star_surcharge line 42
lemma OAI.HyperbolicObstruction.IncidenceTemplate.star_leaf_actual_gap line 49

theorem OAI.HyperbolicObstruction.PinnedAssignments.relative_variance line 75

Source documentation

The generic variance estimate after pinning named coordinates, with the cardinality bound produced from fieldwise injectivity.

theorem relative_variance (tag : W → F) (P : Finset W) (ξ : W → A)
    (hξ : PinFieldwise tag P ξ) (hN : 4 * Fintype.card W ≤ Fintype.card A)
    (row : (W → A) → S → I) (E : S → Finset W)
    (read : ∀ σ τ s, row σ s = row τ s → ∀ v ∈ E s, σ v = τ v)
    (inj : ∀ σ, Fieldwise tag σ → Function.Injective (row σ))
    (p : I → ℝ) (hp : ∀ i, p i ∈ Set.Icc (0 : ℝ) 1) (c : S → ℝ)
    (prob : ∀ σ s, p (row σ s) = (Fintype.card A : ℝ) ^ (-c s))
    {ε : ℝ} (gap : ∀ J : Finset S, J.Nonempty →
      ε ≤ (((J.biUnion E) \ P).card : ℝ) - ∑ s ∈ J, c s) :
    (FiniteLaw.bernoulliProduct p hp).variance
      (fun w => (BernoulliCandidates.count (fun σ => row (extend P ξ σ)) (candidates tag P ξ) w : ℝ)) ≤
    Fintype.card (BernoulliCandidates.OverlapType S) * 2 ^ Fintype.card (Free P) *
…

Mentions: OAI.HyperbolicObstruction.PinnedAssignments.PinFieldwise, OAI.HyperbolicObstruction.PinnedAssignments.Fieldwise, OAI.HyperbolicObstruction.FiniteLaw.bernoulliProduct, OAI.HyperbolicObstruction.BernoulliCandidates.count, OAI.HyperbolicObstruction.PinnedAssignments.extend, OAI.HyperbolicObstruction.PinnedAssignments.candidates, OAI.HyperbolicObstruction.BernoulliCandidates.OverlapType, OAI.HyperbolicObstruction.PinnedAssignments.Free