MultipointAbsorption.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Summation of the pairwise Young bounds. The active index set may change at the individual activation and completion times.

lemma OAI.SLEExactGauge.Multipoint.offDiag_vertex_cost_le line 13

theorem OAI.SLEExactGauge.Multipoint.sum_drift_absorption line 35

Source documentation

Negative one-point drift absorbs every pair contribution. We bound the off-diagonal vertex count by the full square; this only changes the order-dependent choice of epsilon.

theorem sum_drift_absorption {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (D A H : ι → ℝ) (cross weight : ι × ι → ℝ)
    (C k ε L : ℝ) (hε : 0 ≤ ε) (hA : ∀ i ∈ s, 0 ≤ A i)
    (hbudget : 2*ε*(s.card : ℝ) ≤ k)
    (hD : ∀ i ∈ s, D i ≤ C*H i-k*A i)
    (hcross : ∀ ij ∈ s.offDiag, cross ij ≤ ε*(A ij.1+A ij.2)+L*weight ij) :
    (∑ i ∈ s, D i) + (∑ ij ∈ s.offDiag, cross ij) ≤
      C*(∑ i ∈ s, H i) + L*(∑ ij ∈ s.offDiag, weight ij) := by
…

lemma OAI.SLEExactGauge.Multipoint.absorption_epsilon_pos line 53
lemma OAI.SLEExactGauge.Multipoint.absorption_epsilon_budget line 56