ProductBounds.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Combining the scalar sector bounds

Pointwise character bounds multiply over a finite family of leg orders. After normalization by the sum of the singleton exponents, the entropy identity gives the midpoint-concavity bound for the profile.

theorem OAI.MatrixMultiplication.AuxiliarySeparation.finite_product_concavity line 22

Source documentation

Multiplying the entropy bounds and taking the positive normalization root gives the midpoint-concavity inequality.

theorem finite_product_concavity {ι : Type*} [Fintype ι]
    (A B C p : ι → ℝ) {s : ℝ} (hs : 0 < s) (hsum : ∑ i, p i = s)
    (hA : ∀ i, 0 < A i) (hB : ∀ i, 0 < B i) (hC : ∀ i, 0 < C i)
    (hbound : ∀ i q, 0 ≤ q → q ≤ 1 →
      Real.exp (p i * Real.binEntropy q) * (B i) ^ q * (C i) ^ (1 - q) ≤
        (2 : ℝ) ^ (p i) * A i) :
    (∏ i, B i) ^ (1 / s) + (∏ i, C i) ^ (1 / s) ≤
      2 * (∏ i, A i) ^ (1 / s) := by
…

theorem OAI.MatrixMultiplication.AuxiliarySeparation.finite_product_tripling line 73

Source documentation

Multiplying the cyclic bounds and taking the positive normalization root gives the factor of three in the tripling inequality.

theorem finite_product_tripling {ι : Type*} [Fintype ι]
    (A B C p : ι → ℝ) {s : ℝ} (hs : 0 < s) (hsum : ∑ i, p i = s)
    (_hA : ∀ i, 0 < A i) (hB : ∀ i, 0 < B i) (hC : ∀ i, 0 < C i)
    (hbound : ∀ i, (3 : ℝ) ^ p i * B i ^ (2 / 3 : ℝ) * C i ^ (1 / 3 : ℝ) ≤ A i)
    (hprod_eq : ∏ i, C i = ∏ i, B i) :
    3 * (∏ i, B i) ^ (1 / s) ≤ (∏ i, A i) ^ (1 / s) := by
…