Theorem 5.3 at a fixed pair, stationary form
Provedmme_stothers_theorem53_slice_stationary_formDavie--Stothers Theorem 5.3 at a fixed pair, in stationary form.
Let satisfy , let be a strictly positive admissible profile, and let be a strictly positive stationary profile on the same marginal fibre, i.e. . Then for every with
the fourth power has -value at least .
This is the same statement as the slice-infimum form, with the minimality hypothesis on replaced by membership in . The two are interchangeable for the purposes of Theorem 5.3 -- Lemma 5.2 derives minimality from stationarity -- but stationarity is the more useful hypothesis to carry into the extraction: it is exactly what makes an affine function of the nine grade statistics, hence what identifies 's histogram as the maximum-entropy one on the fibre and so what controls the completion-star degree. The factor is the combination loss of Equation (3.4), and it degenerates to exactly on the diagonal , which is the case the published numerical endpoint uses.
import Definitions.Def_mme_stothers_fourth_data open MME universe u set_option autoImplicit false
theorem mme_stothers_theorem53_slice_stationary_form
{K : Type u} [Field K]
(tau : Real) (htauLower : 2 ≤ 3 * tau) (htauUpper : 3 * tau ≤ 3)
(a b : Fin 10 → Real)
(ha : MME.StothersFourth.InZ a)
(hb : MME.StothersFourth.InN b)
(haPos : ∀ i : Fin 10, 0 < a i)
(hbPos : ∀ i : Fin 10, 0 < b i)
(hsame : MME.StothersFourth.InY (fun i => a i - b i)) :
∀ V : Real, 0 ≤ V →
V < MME.StothersFourth.globalRate 6 tau a a *
(MME.StothersFourth.entropyProduct b /
MME.StothersFourth.entropyProduct a) →
HasTauValueAtLeast
(MME.StothersFourth.cwFourthObj K 6) tau V := by
sorry