DegreeCompletion.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Positive completion of a single valid degree

A fixed-degree weight is extended by the constant weight one on every other degree. All off-degree signatures are proved, and all coefficient sums at the original degree are unchanged. This lets the existing general nonnegative-derivative theorem retain contracted coordinates without assuming positivity or signatures of the original weight at other degrees.

def OAI.ContingencyTables.DegreeCompletion.completeDegree line 23
lemma OAI.ContingencyTables.DegreeCompletion.completeDegree_positive line 27
lemma OAI.ContingencyTables.DegreeCompletion.constant_face_signature line 35
lemma OAI.ContingencyTables.DegreeCompletion.completeDegree_face_signature line 47

lemma OAI.ContingencyTables.DegreeCompletion.positive_derivatives_signature line 70

Source documentation

Positive directions are handled by the existing cubic spectral theorem. The cardinality cutoff of a repeated derivative is established at each step.

lemma positive_derivatives_signature (f : Set Γ → ℝ) (hf : ∀ A, 0 < f A)
    (hsig : ∀ A, CommonBasesFPRAS.OnePositive (faceHessian f A).toBilin')
    (ds : List (Γ → ℝ)) (hds : ∀ a ∈ ds, ∀ i, 0 < a i) :
    FullPositive (coeffDerivs ds f) ds.length ∧
      ∀ A, CommonBasesFPRAS.OnePositive (faceHessian (coeffDerivs ds f) A).toBilin' := by
…

Mentions: OAI.CommonBasesFPRAS.OnePositive

lemma OAI.ContingencyTables.DegreeCompletion.nonnegative_derivatives_signature line 89

Source documentation

The zero coordinates of a direction are reached by an actual positive perturbation and the proved closedness of the quadratic signature.

lemma nonnegative_derivatives_signature (f : Set Γ → ℝ) (hf : ∀ A, 0 < f A)
    (hsig : ∀ A, CommonBasesFPRAS.OnePositive (faceHessian f A).toBilin')
    (ds : List (Γ → ℝ)) (hds : ∀ a ∈ ds, ∀ i, 0 ≤ a i) (A : Set Γ) :
    CommonBasesFPRAS.OnePositive (faceHessian (coeffDerivs ds f) A).toBilin' := by
…

Mentions: OAI.CommonBasesFPRAS.OnePositive

theorem OAI.ContingencyTables.DegreeCompletion.completeDegree_hasSlotSignature line 118
Source documentation
All retained-coordinate slot signatures of the completion are proved. The original input is only the single valid-degree addition property.
```
theorem completeDegree_hasSlotSignature (f : Set Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hsig : AdditionProperty f k) :
    HasSlotSignature (completeDegree f k) := by
…
```
Mentions: OAI.ContingencyTables.DegreeCompletion.completeDegree

lemma OAI.ContingencyTables.DegreeCompletion.coeffDerivs_degree_congr line 130

Source documentation

Every nonzero derivative term adds precisely one new element; no fresh-pair or disjointness assumption is needed for this congruence.

lemma coeffDerivs_degree_congr (ds : List (Γ → ℝ)) (f g : Set Γ → ℝ) (k : ℕ)
    (heq : ∀ S, S.ncard = k → f S = g S) (A : Set Γ)
    (hdegree : A.ncard + ds.length = k) : coeffDerivs ds f A = coeffDerivs ds g A := by
…

lemma OAI.ContingencyTables.DegreeCompletion.slotTotal_completeDegree line 149

theorem OAI.ContingencyTables.DegreeCompletion.slot_face_signature_degree line 159

Source documentation

The full retained-coordinate matrix at its valid degree inherits the signature, including coordinates of previously contracted pairs.

theorem slot_face_signature_degree (ps : List (Γ × Γ)) (f : Set Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hsig : AdditionProperty f k) (A : Set Γ)
    (hdegree : A.ncard + ps.length + 2 = k) :
    CommonBasesFPRAS.OnePositive (faceHessian (slotTotal ps f) A).toBilin' := by
…

Mentions: OAI.CommonBasesFPRAS.OnePositive

lemma OAI.ContingencyTables.DegreeCompletion.slotDefect_completeDegree line 175

theorem OAI.ContingencyTables.DegreeCompletion.slotDefect_pair_bound_degree line 193

Source documentation

Actual two-pair masses satisfy the determinant bound on their valid cardinality layer; completion disappears from the conclusion.

theorem slotDefect_pair_bound_degree (ps : List (Γ × Γ)) (f : Set Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hsig : AdditionProperty f k)
    (A : Set Γ) (hdegree : A.ncard + ps.length = k) (hps : SlotsFresh ps A)
    (p r : Γ × Γ) (hp : p ∈ ps) (hr : r ∈ ps) (hpr : p ≠ r) :
    4 * slotDefect ps f A p r * slotDefect ps f A r p ≤ (slotTotal ps f A)^2 := by
…

theorem OAI.ContingencyTables.DegreeCompletion.slotDefect_triple_bound_degree line 206

Source documentation

Actual three-pair masses satisfy the cross-entry bound, obtained from full cubic contraction while retaining the contracted pair coordinates.

theorem slotDefect_triple_bound_degree (ps : List (Γ × Γ)) (f : Set Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hsig : AdditionProperty f k)
    (A : Set Γ) (hdegree : A.ncard + ps.length = k) (hps : SlotsFresh ps A)
    (p r t : Γ × Γ) (hp : p ∈ ps) (hr : r ∈ ps) (ht : t ∈ ps)
    (hpr : p ≠ r) (hrt : r ≠ t) (hpt : p ≠ t) :
    slotDefect ps f A p r * slotDefect ps f A r t ≤
      slotTotal ps f A * slotDefect ps f A p t := by
…