theorem infimalConvolutionFamily_eq_Ah {n m : ℕ} (f : Fin m → (Fin n → ℝ) → EReal) : have e := blockEquivFun; have A := sumLinearMapFun ∘ₗ ↑e; have h := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f i (e x i); have Ah := fun (y : Fin n → ℝ) => sInf {z : EReal | ∃ (x : Fin (m * n) → ℝ), A x = y ∧ z = h x}; Ah = infimalConvolutionFamily f

The infimal convolution family is the linear-map infimum for the block sum.

theorem hA_from_hzero {n m : ℕ} {f0_plus : Fin m → (Fin n → ℝ) → EReal} (hzero : ∀ (z : Fin m → Fin n → ℝ), ∑ i : Fin m, f0_plus i (z i) ≤ 0 → ∑ i : Fin m, f0_plus i (-z i) > 0 → ∑ i : Fin m, z i ≠ 0) : have e := blockEquivFun; have A := sumLinearMapFun ∘ₗ ↑e; have h0_plus := fun (x : Fin (m * n) → ℝ) => ∑ i : Fin m, f0_plus i (e x i); ∀ (z : Fin (m * n) → ℝ), h0_plus z ≤ 0 → h0_plus (-z) > 0 → A z ≠ 0

The h0_plus kernel condition for the block sum follows from the corollary hypothesis.

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

Linear map sending (xᵢ, μᵢ) to (xᵢ, ∑ μᵢ).

Equations

• sumMuLinearMap = { toFun := fun (x : Fin m → (Fin n → ℝ) × ℝ) => (fun (i : Fin m) => (x i).1, ∑ i : Fin m, (x i).2), map_add' := ⋯, map_smul' := ⋯ }

theorem recessionCone_pi_eq_pi_recessionCone {m : ℕ} {E : Type u_1} [AddCommGroup E] [Module ℝ E] (C : Fin m → Set E) (hC : ∀ (i : Fin m), (C i).Nonempty) : (Set.univ.pi C).recessionCone = Set.univ.pi fun (i : Fin m) => (C i).recessionCone

Recession cone of a nonempty product set is the product of recession cones.

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

Sum of real coefficients coerced to EReal is the coercion of the real sum.

theorem sum_ne_bot_of_ne_bot' {α : Type u_1} (s : Finset α) (β : α → EReal) (h : ∀ i ∈ s, β i ≠ ⊥) : s.sum β ≠ ⊥

A finite sum of EReal terms is not ⊥ if none of the terms is ⊥.

theorem sum_eq_top_of_eq_top {α : Type u_1} (s : Finset α) (β : α → EReal) (i0 : α) (hi0 : i0 ∈ s) (htop : β i0 = ⊤) (hbot : ∀ i ∈ s, β i ≠ ⊥) : s.sum β = ⊤

A finite sum is ⊤ if one term is ⊤ and none are ⊥.

theorem split_real_sum_of_le {m : ℕ} (hm : 0 < m) {β : Fin m → EReal} {α : ℝ} (hbot : ∀ (i : Fin m), β i ≠ ⊥) (hβ : ∑ i : Fin m, β i ≤ ↑α) : ∃ (a : Fin m → ℝ), (∀ (i : Fin m), β i ≤ ↑(a i)) ∧ ∑ i : Fin m, a i = α

Split a real upper bound on an EReal sum into componentwise real bounds.

theorem g0_plus_gt_toReal_sum {m : ℕ} {β : Fin m → EReal} {α : ℝ} (hnot_top : ∀ (i : Fin m), β i ≠ ⊤) (hnot_bot : ∀ (i : Fin m), β i ≠ ⊥) : ∑ i : Fin m, β i > ↑α ↔ ∑ i : Fin m, (β i).toReal > α

A strict inequality on a finite EReal sum is equivalent to the strict real inequality.

theorem split_real_sum_of_gt {m : ℕ} (hm : 0 < m) {r : Fin m → ℝ} {α : ℝ} : ∑ i : Fin m, r i > α → ∃ (i0 : Fin m) (a : Fin m → ℝ), a i0 < r i0 ∧ (∀ (i : Fin m), i ≠ i0 → a i = r i) ∧ ∑ i : Fin m, a i = α

Split a strict inequality for a real sum by lowering one component.

theorem split_real_sum_of_gt_strict_all {m : ℕ} (hm : 0 < m) {r : Fin m → ℝ} {α : ℝ} (hgt : ∑ i : Fin m, r i > α) : ∃ (a : Fin m → ℝ), (∀ (i : Fin m), a i < r i) ∧ ∑ i : Fin m, a i = α

Split a strict sum inequality into strictly lower components with the same total.

theorem not_mem_recessionCone_epigraph_witness {n : ℕ} {f : (Fin n → ℝ) → EReal} {v : Fin n → ℝ} {a : ℝ} (hnot : (v, a) ∉ (epigraph Set.univ f).recessionCone) : ∃ (x : Fin n → ℝ) (μ : ℝ) (t : ℝ), 0 ≤ t ∧ f (x + t • v) > ↑(μ + t * a) ∧ f x ≤ ↑μ

A witness for failing recession membership in an epigraph.

theorem nonempty_epigraph_of_hrec {n m : ℕ} {f f0_plus : Fin m → (Fin n → ℝ) → EReal} (hnotbot0 : ∀ (i : Fin m) (x : Fin n → ℝ), f0_plus i x ≠ ⊥) (hrec_i : ∀ (i : Fin m), (epigraph Set.univ (f i)).recessionCone = epigraph Set.univ (f0_plus i)) (i : Fin m) : (epigraph Set.univ (f i)).Nonempty

Epigraph nonemptiness from recession-epigraph equality and non-bottomness.

theorem mem_recessionCone_of_add_mem_fixed_t {E : Type u_1} [AddCommGroup E] [Module ℝ E] {C : Set E} (hconv : Convex ℝ C) {v : E} {t : ℝ} (ht : 0 < t) (hadd : ∀ x ∈ C, x + t • v ∈ C) : v ∈ C.recessionCone

A fixed-step translation in a convex set yields a recession direction.

theorem recCone_tight_approx_at_t {n : ℕ} {f f0_plus : (Fin n → ℝ) → EReal} (hrec : (epigraph Set.univ f).recessionCone = epigraph Set.univ f0_plus) (hconv : Convex ℝ (epigraph Set.univ f)) {v : Fin n → ℝ} {a : ℝ} (ha : ↑a < f0_plus v) {t : ℝ} (ht : 0 < t) {ε : ℝ} (hε : 0 < ε) : ∃ (x : Fin n → ℝ) (μ : ℝ), f x ≤ ↑μ ∧ ↑(μ + t * a - ε) ≤ f (x + t • v)

Approximate a recession slope at a fixed time with slack.

theorem strict_sum_from_one_component_with_slack {m : ℕ} {β b ε : Fin m → ℝ} {i0 : Fin m} (hgt : β i0 > b i0) (hslack : ∀ (i : Fin m), i ≠ i0 → β i ≥ b i - ε i) (hε : ∑ i ∈ Finset.univ.erase i0, ε i < β i0 - b i0) : ∑ i : Fin m, β i > ∑ i : Fin m, b i

A strict gap at one component plus slack bounds on the others yields a strict sum.

theorem ereal_strict_sum_from_one_component_with_slack {m : ℕ} {β : Fin m → EReal} {b ε : Fin m → ℝ} {i0 : Fin m} (hnot_top : ∀ (i : Fin m), β i ≠ ⊤) (hnot_bot : ∀ (i : Fin m), β i ≠ ⊥) (hgt : β i0 > ↑(b i0)) (hslack : ∀ (i : Fin m), i ≠ i0 → β i ≥ ↑(b i - ε i)) (hε : ∑ i ∈ Finset.univ.erase i0, ε i < (β i0).toReal - b i0) : ∑ i : Fin m, β i > ∑ i : Fin m, ↑(b i)

A strict gap with slack on EReal components yields a strict sum inequality.

theorem recessionCone_sum_epigraph_prod_top_contra {n m : ℕ} {f f0_plus : Fin m → (Fin n → ℝ) → EReal} {g : (Fin m → Fin n → ℝ) → EReal} (hg : g = fun (x : Fin m → Fin n → ℝ) => ∑ i : Fin m, f i (x i)) (hnotbot : ∀ (i : Fin m) (x : Fin n → ℝ), f i x ≠ ⊥) (_hnotbot0 : ∀ (i : Fin m) (x : Fin n → ℝ), f0_plus i x ≠ ⊥) (_hrec_i : ∀ (i : Fin m), (epigraph Set.univ (f i)).recessionCone = epigraph Set.univ (f0_plus i)) {p : (Fin m → Fin n → ℝ) × ℝ} {i0 : Fin m} (_htop : f0_plus i0 (p.1 i0) = ⊤) {a : Fin m → ℝ} {x0 : Fin n → ℝ} {μ0 t : ℝ} (hgt0 : f i0 (x0 + t • p.1 i0) > ↑(μ0 + t * a i0)) (_hx0 : f i0 x0 ≤ ↑μ0) (ha_sum : ∑ i : Fin m, a i = p.2) {x : Fin m → Fin n → ℝ} {μ : Fin m → ℝ} (hxi0 : x i0 = x0) (hμi0 : μ i0 = μ0) (_hxle : ∀ (i : Fin m), f i (x i) ≤ ↑(μ i)) {ε : Fin m → ℝ} (hslack : ∀ (i : Fin m), i ≠ i0 → ↑(μ i + t * a i - ε i) ≤ f i (x i + t • p.1 i)) (hε : ∑ i ∈ Finset.univ.erase i0, ε i < (f i0 (x0 + t • p.1 i0)).toReal - (μ0 + t * a i0)) (hmem''' : g (x + t • p.1) ≤ ↑(∑ i : Fin m, μ i) + ↑t * ↑p.2) (htopg : ¬∃ (i : Fin m), f i (x i + t • p.1 i) = ⊤) : False

Finite-case contradiction in the ⊤ branch of recessionCone_sum_epigraph_prod.