@[simp]

theorem section16_euclideanSpace_equiv_toLp {n : ℕ} (x : Fin n → ℝ) : (EuclideanSpace.equiv (Fin n) ℝ) (WithLp.toLp 2 x) = x

The Euclidean-space equivalence reduces to the identity on Fin n → ℝ.

@[simp]

theorem section16_euclideanSpace_equiv_symm_apply {n : ℕ} (x : Fin n → ℝ) : (EuclideanSpace.equiv (Fin n) ℝ).symm x = WithLp.toLp 2 x

The inverse Euclidean-space equivalence reduces to WithLp.toLp.

theorem section16_exists_image_mem_ri_effectiveDomain_iff_not_exists_adjoint_eq_zero_recession_ineq {n m : ℕ} (A : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin m)) (g : (Fin m → ℝ) → EReal) (hg : ProperConvexFunctionOn Set.univ g) : (¬∃ (yStar : EuclideanSpace ℝ (Fin m)), (LinearMap.adjoint A) yStar = 0 ∧ recessionFunction (fenchelConjugate m g) yStar.ofLp ≤ 0 ∧ recessionFunction (fenchelConjugate m g) (-yStar.ofLp) > 0) ↔ ∃ (x : EuclideanSpace ℝ (Fin n)), A x ∈ euclideanRelativeInterior m ((fun (z : EuclideanSpace ℝ (Fin m)) => z.ofLp) ⁻¹' effectiveDomain Set.univ g)

Corollary 16.2.1. Let A be a linear transformation from ℝ^n to ℝ^m and let g be a proper convex function on ℝ^m. Then there exists no vector y* ∈ ℝ^m such that

A^* y* = 0, (g^*0^+)(y*) ≤ 0, and (g^*0^+)(-y*) > 0

if and only if A x ∈ ri (dom g) for at least one x ∈ ℝ^n.

Here dom g is the effective domain effectiveDomain univ g, ri is euclideanRelativeInterior, and (g^*0^+) is represented as recessionFunction (fenchelConjugate m g).

noncomputable def section16_blockEquivFun {n m : ℕ} : (Fin (m * n) → ℝ) ≃ₗ[ℝ] Fin m → Fin n → ℝ

Block equivalence between flattened vectors and block families.

Equations

• section16_blockEquivFun = blockEquivFun

noncomputable def section16_blockLinearMap {n m : ℕ} (i : Fin m) : (Fin (m * n) → ℝ) →ₗ[ℝ] Fin n → ℝ

Block projection linear map extracting the i-th block.

Equations

• section16_blockLinearMap i = LinearMap.proj i ∘ₗ ↑section16_blockEquivFun

noncomputable def section16_unblock {n m : ℕ} : (Fin m → Fin n → ℝ) →ₗ[ℝ] Fin (m * n) → ℝ

Flatten a block family into a single vector.

Equations

• section16_unblock = ↑section16_blockEquivFun.symm

theorem section16_blockLinearMap_unblock {n m : ℕ} (i : Fin m) (x : Fin m → Fin n → ℝ) : (section16_blockLinearMap i) (section16_unblock x) = x i

Unblocking followed by block projection recovers the original block.

theorem section16_unblock_blockLinearMap {n m : ℕ} (x : Fin (m * n) → ℝ) : (section16_unblock fun (i : Fin m) => (section16_blockLinearMap i) x) = x

Unblocking the block projections recovers the original vector.

noncomputable def section16_diagBlockLinearMap {n m : ℕ} : (Fin n → ℝ) →ₗ[ℝ] Fin m → Fin n → ℝ

Diagonal block embedding sending x to the constant block family.

Equations

• section16_diagBlockLinearMap = { toFun := fun (x : Fin n → ℝ) (x_1 : Fin m) => x, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def section16_diagLinearMap {n m : ℕ} : (Fin n → ℝ) →ₗ[ℝ] Fin (m * n) → ℝ

Diagonal embedding into the flattened space.

Equations

• section16_diagLinearMap = section16_unblock ∘ₗ section16_diagBlockLinearMap

theorem section16_blockLinearMap_diag {n m : ℕ} (i : Fin m) (x : Fin n → ℝ) : (section16_blockLinearMap i) (section16_diagLinearMap x) = x

Block projection of the diagonal embedding is the identity.

theorem section16_blockLinearMap_surjective {n m : ℕ} (i : Fin m) : Function.Surjective ⇑(section16_blockLinearMap i)

Each block projection is surjective.

noncomputable def section16_diagLinearMapE {n m : ℕ} : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin (m * n))

Diagonal embedding as a linear map on Euclidean space.

Equations

• section16_diagLinearMapE = ↑(EuclideanSpace.equiv (Fin (m * n)) ℝ).symm.toLinearEquiv ∘ₗ section16_diagLinearMap ∘ₗ ↑(EuclideanSpace.equiv (Fin n) ℝ).toLinearEquiv

noncomputable def section16_blockLinearMapE {n m : ℕ} (i : Fin m) : EuclideanSpace ℝ (Fin (m * n)) →ₗ[ℝ] EuclideanSpace ℝ (Fin n)

Block projection as a linear map on Euclidean space.

Equations

• section16_blockLinearMapE i = ↑(EuclideanSpace.equiv (Fin n) ℝ).symm.toLinearEquiv ∘ₗ section16_blockLinearMap i ∘ₗ ↑(EuclideanSpace.equiv (Fin (m * n)) ℝ).toLinearEquiv

theorem section16_diagLinearMapE_apply {n m : ℕ} (x : EuclideanSpace ℝ (Fin n)) : (section16_diagLinearMapE x).ofLp = section16_diagLinearMap x.ofLp

Coercion form of the diagonal map.

theorem section16_blockLinearMapE_apply {n m : ℕ} (i : Fin m) (y : EuclideanSpace ℝ (Fin (m * n))) : ((section16_blockLinearMapE i) y).ofLp = (section16_blockLinearMap i) y.ofLp

Coercion form of the block projection.

theorem section16_blockLinearMapE_diag {n m : ℕ} (i : Fin m) (x : EuclideanSpace ℝ (Fin n)) : (section16_blockLinearMapE i) (section16_diagLinearMapE x) = x

Block projection of the diagonal embedding is the identity on Euclidean space.

theorem section16_blockLinearMap_apply_equiv {n m : ℕ} (i : Fin m) (x : Fin (m * n) → ℝ) (j : Fin n) : (section16_blockLinearMap i) x j = x ((Fintype.equivFinOfCardEq ⋯) (i, j))

Evaluate the block projection via the canonical index equivalence.

theorem section16_unblock_apply_equiv {n m : ℕ} (xStar : Fin m → Fin n → ℝ) (i : Fin m) (j : Fin n) : section16_unblock xStar ((Fintype.equivFinOfCardEq ⋯) (i, j)) = xStar i j

Evaluate unblocking via the canonical index equivalence.

theorem section16_dotProduct_unblock_eq_sum_blocks {n m : ℕ} (xStar : Fin m → Fin n → ℝ) (x : Fin (m * n) → ℝ) : x ⬝ᵥ section16_unblock xStar = ∑ i : Fin m, (section16_blockLinearMap i) x ⬝ᵥ xStar i

Dot product against an unblocked vector splits by blocks.

theorem section16_dotProduct_unblock_eq_sum_blocks_symm {n m : ℕ} (xStar : Fin m → Fin n → ℝ) (x : Fin (m * n) → ℝ) : section16_unblock xStar ⬝ᵥ x = ∑ i : Fin m, xStar i ⬝ᵥ (section16_blockLinearMap i) x

Dot product with an unblocked vector splits symmetrically by blocks.

theorem section16_diagLinearMapE_adjoint_eq_sum_blockLinearMapE {n m : ℕ} : LinearMap.adjoint section16_diagLinearMapE = ∑ i : Fin m, section16_blockLinearMapE i

The adjoint of the diagonal embedding is the sum of block projections.

theorem section16_effectiveDomain_blockSum_eq_iInter_preimage_blocks {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) : have g := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i ((section16_blockLinearMap i) x); effectiveDomain Set.univ g = ⋂ (i : Fin m), ⇑(section16_blockLinearMap i) ⁻¹' effectiveDomain Set.univ (f i)

Effective domain of a block-sum is the intersection of block preimages.

theorem section16_properConvexFunctionOn_blockSum {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : ProperConvexFunctionOn Set.univ fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i ((section16_blockLinearMap i) x)

Properness of the block-sum function assembled from proper convex summands.

theorem section16_blockLinearMapE_image_effectiveDomain_blockSum_eq {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) (i : Fin m) : have g := fun (x : Fin (m * n) → ℝ) => ∑ j : Fin m, f j ((section16_blockLinearMap j) x); ⇑(section16_blockLinearMapE i) '' ((fun (z : EuclideanSpace ℝ (Fin (m * n))) => z.ofLp) ⁻¹' effectiveDomain Set.univ g) = (fun (x : EuclideanSpace ℝ (Fin n)) => x.ofLp) ⁻¹' effectiveDomain Set.univ (f i)

Image of the block projection on the block-sum effective domain.

theorem section16_sum_coe {ι : Type u_1} (s : Finset ι) (f : ι → ℝ) : ∑ i ∈ s, ↑(f i) = ↑(s.sum f)

Coercion from ℝ to EReal commutes with finite sums.

theorem section16_sSup_image2_add_eq_sSup_add {S T : Set EReal} : sSup (Set.image2 (fun (x1 x2 : EReal) => x1 + x2) S T) = sSup S + sSup T

Supremum of pairwise sums in EReal splits as the sum of suprema.

theorem section16_supportFunction_effectiveDomain_blockSum_unblock_ge_sum {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (xStar : Fin m → Fin n → ℝ) (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) : have g := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i ((section16_blockLinearMap i) x); ∑ i : Fin m, supportFunctionEReal (effectiveDomain Set.univ (f i)) (xStar i) ≤ supportFunctionEReal (effectiveDomain Set.univ g) (section16_unblock xStar)

Support function of a block-sum domain dominates the sum of blockwise support functions.

theorem section16_supportFunction_effectiveDomain_blockSum_unblock_eq_sum {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (xStar : Fin m → Fin n → ℝ) (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) : have g := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i ((section16_blockLinearMap i) x); supportFunctionEReal (effectiveDomain Set.univ g) (section16_unblock xStar) = ∑ i : Fin m, supportFunctionEReal (effectiveDomain Set.univ (f i)) (xStar i)

Support function of a block-sum effective domain splits by blocks.

theorem section16_recession_blockSum_unblock_eq_sum {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) (xStar : Fin m → Fin n → ℝ) (hf : ∀ (i : Fin m), ProperConvexFunctionOn Set.univ (f i)) : have g := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i ((section16_blockLinearMap i) x); recessionFunction (fenchelConjugate (m * n) g) (section16_unblock xStar) = ∑ i : Fin m, recessionFunction (fenchelConjugate n (f i)) (xStar i)

Recession of the block-sum conjugate splits by blocks at an unblocked covector.