BandStateMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One exact finite transfer step for reciprocal masses of truncated states.

lemma OAI.TotientAsymptotic.factorProduct_band_split line 11
lemma OAI.TotientAsymptotic.state_fiber_reciprocal line 23

theorem OAI.TotientAsymptotic.band_state_mass_transfer line 50

Source documentation

Summing on the image of the next state avoids charging old multiplicities again.

theorem band_state_mass_transfer {b k : ℕ} (hk : k ≤ b) {U V A : ℝ} (hUV : U ≤ V)
    (Q : Finset (ShiftedPair b))
    (hQ : ∀ t ∈ Q,∀ j,partBelow (t.left j) V=t.left j ∧ partBelow (t.right j) V=t.right j)
    (htail : ∀ t ∈ Q,∀ j : Fin b,k ≤ j.val →
      partBetween (t.left j) U V=1 ∧ partBetween (t.right j) U V=1)
    (hband : ∀ r ∈ Q.image (fun t => lowerState t U),
      (∑ f ∈ (Q.filter (fun t => lowerState t U=r)).image (fun t => stateBand hk t U V),
        (pairedProduct f:ℝ)⁻¹) ≤ A) :
    (∑ t ∈ Q,(factorProduct t:ℝ)⁻¹) ≤
      A*(∑ r ∈ Q.image (fun t => lowerState t U),(factorProduct r:ℝ)⁻¹) := by
…

Mentions: OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.partBelow, OAI.TotientAsymptotic.partBetween, OAI.TotientAsymptotic.lowerState, OAI.TotientAsymptotic.stateBand, OAI.TotientAsymptotic.pairedProduct, OAI.TotientAsymptotic.factorProduct