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 MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finite_product_concavity {ι : Type u_1} [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)

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

theorem MatrixMultiplicationAllFields.MatrixMultiplication.AuxiliarySeparation.finite_product_tripling {ι : Type u_1} [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)

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