OAI/Combinatorics/ContingencyTables/Transport/NestedPenaltyApplication.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The first paper's actual positive penalties and hard equality limit

Full row/column deviations give absolute affine line factors; the nested small-slot residual constraints give positive-part affine factors. Their product is exactly 2^(-L D). Balanced large-slot sums retain their proved signature, and their finite limit is the exact zero-penalty indicator sum.

  1. def OAI.ContingencyTables.NestedPenaltyApplication.penalty line 27
  2. def OAI.ContingencyTables.NestedPenaltyApplication.softWeight line 32
  3. def OAI.ContingencyTables.NestedPenaltyApplication.hardWeight line 38
  4. lemma OAI.ContingencyTables.NestedPenaltyApplication.penalty_nonnegative line 42
  5. lemma OAI.ContingencyTables.NestedPenaltyApplication.prod_pow line 49
  6. theorem OAI.ContingencyTables.NestedPenaltyApplication.softWeight_eq line 57

    Source documentation

    This is the manuscript's literal exponential of the full deviation plus the small residual violation penalty, with eta=2^(-L).

    theorem softWeight_eq (line : C → G) (inner : C → Bool)
    (offset slope smallOffset smallSlope : G → ℝ) (L : ℝ) (z : C → ℕ) :
    softWeight line inner offset slope smallOffset smallSlope L z =
      (2:ℝ)^(-L*penalty line inner offset slope smallOffset smallSlope z) := by
…

    Mentions: OAI.ContingencyTables.NestedPenaltyApplication.softWeight, OAI.ContingencyTables.NestedPenaltyApplication.penalty

  7. lemma OAI.ContingencyTables.NestedPenaltyApplication.softWeight_positive line 66
  8. theorem OAI.ContingencyTables.NestedPenaltyApplication.softWeight_removal line 72
  9. theorem OAI.ContingencyTables.NestedPenaltyApplication.softWeight_tendsto line 82
  10. theorem OAI.ContingencyTables.NestedPenaltyApplication.softened_marginal_slices line 93

    Source documentation

    The actual softened marginal is positive before the hard limit and has the raw integer removal signature on every required display.

    theorem softened_marginal_slices (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (line : Coordinates I Ms → G) (inner : Coordinates I Ms → Bool)
    (offset slope smallOffset smallSlope : G → ℝ) (L : ℝ) (hL : 0 ≤ L)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M) :
    PositiveSlice (eliminate Ms (softWeight line inner offset slope smallOffset smallSlope L)) m R ∧
      RemovalSlice (eliminate Ms (softWeight line inner offset slope smallOffset smallSlope L)) m R := by
…

    Mentions: OAI.ContingencyTables.NestedPenaltyApplication.softWeight

  11. theorem OAI.ContingencyTables.NestedPenaltyApplication.hard_marginal_removal line 107

    Source documentation

    The first paper's hard-zero finite marginal inherits its actual raw signature. This proves the required input to factorial omission lifting.

    theorem hard_marginal_removal (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (line : Coordinates I Ms → G) (inner : Coordinates I Ms → Bool)
    (offset slope smallOffset smallSlope : G → ℝ)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M) :
    RemovalSlice (eliminate Ms (hardWeight line inner offset slope smallOffset smallSlope)) m R := by
…

    Mentions: OAI.ContingencyTables.NestedPenaltyApplication.hardWeight

  12. theorem OAI.ContingencyTables.NestedPenaltyApplication.truncate_softened_marginal line 124

    Source documentation

    Zero extension outside the box and full total gives precisely the same actual softened marginal on its required state slice.

    theorem truncate_softened_marginal (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (line : Coordinates I Ms → G) (inner : Coordinates I Ms → Bool)
    (offset slope smallOffset smallSlope : G → ℝ) (L : ℝ)
    (z : I → ℕ) (hz : InBox m z) (htotal : (∑ i, z i)=R) :
    eliminate Ms
      (IntegerBoxTruncation.truncate
        (softWeight line inner offset slope smallOffset smallSlope L) (bounds m Ms) (R+Ms.sum)) z =
      eliminate Ms (softWeight line inner offset slope smallOffset smallSlope L) z := by
…

    Mentions: OAI.ContingencyTables.IntegerBoxTruncation.truncate, OAI.ContingencyTables.NestedPenaltyApplication.softWeight

  13. theorem OAI.ContingencyTables.NestedPenaltyApplication.softened_firstLift_data line 138

    Source documentation

    The actual softened factorial lift now has both required properties by the integer proofs above; neither binary property is assumed.

    theorem softened_firstLift_data {L : Type*} [Fintype L] (group : L → I)
    (Ms : List ℕ) (R : ℕ) (D : ℝ) (hD : 0 < D)
    (line : Coordinates I Ms → G) (inner : Coordinates I Ms → Bool)
    (offset slope smallOffset smallSlope : G → ℝ) (a : ℝ) (ha : 0 ≤ a)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M) :
    let f := LabelledFactorial.firstLift group
…

    Mentions: OAI.ContingencyTables.LabelledFactorial.firstLift

  14. theorem OAI.ContingencyTables.NestedPenaltyApplication.firstLift_limit line 155

    Source documentation

    These are the literal subset weights consumed by endpoint-positive hard-zero transport, with no positivity requirement on internal limits.

    theorem firstLift_limit {L : Type*} [Fintype L] (group : L → I)
    (Ms : List ℕ) (D : ℝ) (line : Coordinates I Ms → G) (inner : Coordinates I Ms → Bool)
    (offset slope smallOffset smallSlope : G → ℝ) (S : Set L) :
    Tendsto (fun a : ℝ => LabelledFactorial.firstLift group
      (eliminate Ms (softWeight line inner offset slope smallOffset smallSlope a)) D S) atTop
      (nhds (LabelledFactorial.firstLift group
        (eliminate Ms (hardWeight line inner offset slope smallOffset smallSlope)) D S)) := by
…

    Mentions: OAI.ContingencyTables.LabelledFactorial.firstLift, OAI.ContingencyTables.NestedPenaltyApplication.softWeight, OAI.ContingencyTables.NestedPenaltyApplication.hardWeight

  15. theorem OAI.ContingencyTables.NestedPenaltyApplication.hard_firstLift_transport line 170

    Source documentation

    Actual first-paper hard transport. The positive softened factorial properties are proved above from the explicit deviation penalties. Only the two hard limiting endpoint masses are required to be positive.

    theorem hard_firstLift_transport {L : Type*} [Fintype L]
    (group : L → I) (Ms : List ℕ) (R : ℕ) (D : ℝ) (hD : 0 < D)
    (line : Coordinates I Ms → G) (inner : Coordinates I Ms → Bool)
    (offset slope smallOffset smallSlope : G → ℝ) (hwidth : ∀ M ∈ Ms, 2 ≤ M)
    (ps : List (L × L)) (H : Set L → ℝ) (A : Set L) (p d : L) (W : L → ℝ)
    (hR : R ≤ Fintype.card L) (hdegree : A.ncard+ps.length+1=Fintype.card L-R)
    (hpd : p≠d) (hpA : p∉A) (hdA : d∉A)
    (hps : CommonBasesFPRAS.SlotsFresh ps (A ∪ Set.range (CommonBasesFPRAS.rootEmbedding p d)))
    (hW : ∀ i, 0 < W i) (hw : ∀ a∈ps, W a.1=W a.2)
    (hsp : 0 < CommonBasesFPRAS.slotTotal ps
      (BinaryContraction.complementWeight (LabelledFactorial.firstLift group
        (eliminate Ms (hardWeight line inner offset slope smallOffset smallSlope)) D)) (insert p A))
…

    Mentions: OAI.CommonBasesFPRAS.SlotsFresh, OAI.CommonBasesFPRAS.rootEmbedding, OAI.CommonBasesFPRAS.slotTotal, OAI.ContingencyTables.BinaryContraction.complementWeight, OAI.ContingencyTables.LabelledFactorial.firstLift, OAI.ContingencyTables.NestedPenaltyApplication.hardWeight