RecursiveSignedTransport.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Recursive signed transport for fixed-degree weights

The recursive transport construction of the bounded-table counting paper uses positivity at the valid subset degree. Signatures after pair summation follow from that degree's addition property and full cubic contraction.

lemma OAI.ContingencyTables.RecursiveSignedTransport.slotTotal_degree_positive line 20
lemma OAI.ContingencyTables.RecursiveSignedTransport.embedded_union_card line 42

theorem OAI.ContingencyTables.RecursiveSignedTransport.slot_pair_signature line 53

Source documentation

The exact signature needed by the recursion, obtained after summing fresh pairs only on the valid residual degree.

theorem slot_pair_signature (ps : List (Γ × Γ)) :
    ∀ {κ : Type*} [Fintype κ] [DecidableEq κ] [Nonempty κ]
      (f : Set Γ → ℝ) (k : ℕ) (A : Set Γ) (e : κ → Γ),
      DegreePositive f k → AdditionProperty f k →
      A.ncard + ps.length + 2 = k → Function.Injective e →
      (∀ i, e i ∉ A) → SlotsFresh ps (A ∪ Set.range e) →
      CommonBasesFPRAS.OnePositive (pairMatrix (slotTotal ps f) A e).toBilin' := by
…

Mentions: OAI.CommonBasesFPRAS.OnePositive

lemma OAI.ContingencyTables.RecursiveSignedTransport.slot_split_signature_degree line 176

theorem OAI.ContingencyTables.RecursiveSignedTransport.transport_linear_bound_degree line 205

Source documentation

The full recursive signed transport bound. Every mass and signature is supplied by the proved exact-degree lemmas above, and all future-slot corrections telescope through the actual binary recursion.

theorem transport_linear_bound_degree (ps : List (Γ × Γ)) :
    ∀ {κ : Type*} [Fintype κ] [DecidableEq κ] [Nonempty κ]
      (f H : Set Γ → ℝ) (A : Set Γ) (e : κ → Γ) (h : κ → ℝ) (W : Γ → ℝ) (k : ℕ),
      DegreePositive f k → AdditionProperty f k →
      A.ncard + ps.length + 1 = k → Function.Injective e →
      (∀ i, e i ∉ A) → SlotsFresh ps (A ∪ Set.range e) →
      (∀ i, 0 < W i) → (∀ p ∈ ps, W p.1 = W p.2) →
      (∑ i, slotTotal ps f (insert (e i) A)*h i = 0) →
      2*transportDemand ps f H A e h ≤
        transportPotential ps f A e h W - transportCorrection ps f A e h W +
          transportEnergy ps f H A e W := by
…

theorem OAI.ContingencyTables.RecursiveSignedTransport.transport_squared_bound_degree line 301
lemma OAI.ContingencyTables.RecursiveSignedTransport.rootCoefficient_degree_pos line 322

theorem OAI.ContingencyTables.RecursiveSignedTransport.transport_root_bound_degree line 368

Source documentation

The paper's root transport coefficient and weighted mean difference, with fixed-degree positivity and addition signatures only. For one-hole states this is applied to the complement-set weight.

theorem transport_root_bound_degree (ps : List (Γ × Γ)) (f H : Set Γ → ℝ)
    (A : Set Γ) (p d : Γ) (W : Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hSig : AdditionProperty f k)
    (hdegree : A.ncard + ps.length + 1 = k)
    (hpd : p ≠ d) (hpA : p ∉ A) (hdA : d ∉ A)
    (hps : SlotsFresh ps (A ∪ Set.range (rootEmbedding p d)))
    (hW : ∀ i, 0 < W i) (hw : ∀ p ∈ ps, W p.1 = W p.2) :
    (slotTotal ps (fun S => f S*H S) (insert p A) / slotTotal ps f (insert p A) -
      slotTotal ps (fun S => f S*H S) (insert d A) / slotTotal ps f (insert d A))^2 ≤
    rootCoefficient ps f A p d W * transportEnergy ps f H A (rootEmbedding p d) W := by
…

lemma OAI.ContingencyTables.RecursiveSignedTransport.slotVertices_degree line 410
lemma OAI.ContingencyTables.RecursiveSignedTransport.transportEnergy_le_graphEnergy_degree line 443

theorem OAI.ContingencyTables.RecursiveSignedTransport.transport_graph_bound_degree line 467

Source documentation

Full one-hole transport on the actual exchange graph with the exact minimum-endpoint conductances and unordered-edge convention.

theorem transport_graph_bound_degree (ps : List (Γ × Γ)) (f H : Set Γ → ℝ)
    (A : Set Γ) (p d : Γ) (W : Γ → ℝ) (k : ℕ)
    (hf : DegreePositive f k) (hSig : AdditionProperty f k)
    (hdegree : A.ncard + ps.length + 1 = k)
    (hpd : p ≠ d) (hpA : p ∉ A) (hdA : d ∉ A)
    (hps : SlotsFresh ps (A ∪ Set.range (rootEmbedding p d)))
    (hW : ∀ i, 0 < W i) (hw : ∀ p ∈ ps, W p.1 = W p.2) :
    (slotTotal ps (fun S => f S*H S) (insert p A) / slotTotal ps f (insert p A) -
      slotTotal ps (fun S => f S*H S) (insert d A) / slotTotal ps f (insert d A))^2 ≤
    rootCoefficient ps f A p d W * slotGraphEnergy ps f H A (rootEmbedding p d) W := by
…

theorem OAI.ContingencyTables.RecursiveSignedTransport.one_hole_transport line 489

Source documentation

The one-hole statement in the paper's omission convention. An encoded set is the complement of the original table-lift state, so the multiplier marks its unique hole slot.

theorem one_hole_transport (ps : List (Γ × Γ)) (f H : Set Γ → ℝ)
    (A : Set Γ) (p d : Γ) (W : Γ → ℝ) (k : ℕ)
    (hk : k ≤ Fintype.card Γ) (hf : DegreePositive f k) (hSig : OmissionProperty f k)
    (hdegree : A.ncard + ps.length + 1 = Fintype.card Γ - k)
    (hpd : p ≠ d) (hpA : p ∉ A) (hdA : d ∉ A)
    (hps : SlotsFresh ps (A ∪ Set.range (rootEmbedding p d)))
    (hW : ∀ i, 0 < W i) (hw : ∀ p ∈ ps, W p.1 = W p.2) :
    let fc := complementWeight f
…