RetainedDeletionBridge.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual complex correlation lost at either endpoint is dominated by the positive deletion costs already estimated on integer intervals.

lemma OAI.TwoPointCorrelations.integerEdgeKeep_of_larger_eligibility line 15
lemma OAI.TwoPointCorrelations.liouville_edge_norm_le_positive line 32
def OAI.TwoPointCorrelations.uncutNumericalEdge line 47
lemma OAI.TwoPointCorrelations.norm_sub_optional_le_two_costs line 55
lemma OAI.TwoPointCorrelations.retainedNumericalEdge_optional line 66
lemma OAI.TwoPointCorrelations.retainedNumericalEdge_eq_uncut_of_good line 77
lemma OAI.TwoPointCorrelations.positiveDeletionAtom_eq_good_cost line 108
lemma OAI.TwoPointCorrelations.positiveDeletionAtom_nonneg line 128

theorem OAI.TwoPointCorrelations.uncut_sub_retained_edge_le line 140

Source documentation

On a numerical edge, each discarded correlation is paid by one of its two actual endpoint costs. No averaging or periodicity premise is added.

theorem uncut_sub_retained_edge_le {J : ℕ} (P : Fin J → Finset ℕ)
    (R Q : Finset ℕ) (η : ℝ) (c : ℕ → ℝ) (L K W : ℝ)
    (eligible : ℤ → ℕ → ℕ → Prop) (h : ℕ) (gate : ℕ → ℤ → ℤ → Prop)
    (bad : ℤ → ℤ → Prop) (j : ℤ) (d q : ℕ) (n : ℤ)
    (hsub : ∀ r ∈ R, eligible j d r → actualPaddingBin η (c d) j r)
    (hd : d.primeFactors.card = J) :
    ‖uncutNumericalEdge R (eligible j) h gate d q n (n + (h * q * d : ℕ)) -
      retainedNumericalEdge P R Q actualPaddingCoefficient (eligible j) L K W
        (fun _ => actualPaddingDegreeCut Q L) h gate (fun z => ¬bad j z)
        d q n (n + (h * q * d : ℕ))‖ ≤
      positiveDeletionAtom (primeTuplePool P) Q R η c L K W eligible bad j d q n +
      positiveDeletionAtom (primeTuplePool P) Q R η c L K W eligible bad j d q
…

Mentions: OAI.TwoPointCorrelations.actualPaddingBin, OAI.TwoPointCorrelations.uncutNumericalEdge, OAI.TwoPointCorrelations.retainedNumericalEdge, OAI.TwoPointCorrelations.actualPaddingCoefficient, OAI.TwoPointCorrelations.actualPaddingDegreeCut, OAI.TwoPointCorrelations.positiveDeletionAtom, OAI.TwoPointCorrelations.primeTuplePool