@[implicit_reducible]

noncomputable instance ERealFunction.instZeroForallElemERealIoiBot_convexAnalysisMonotoneOperators_BauschkeCombettes_2017 {H : Type u} : Zero (H → ↑(Set.Ioi ⊥))

The canonical additive identity on ]-∞,+∞]-valued functions is the constant-zero function.

@[implicit_reducible]

noncomputable instance ERealFunction.instAddForallElemERealIoiBot_convexAnalysisMonotoneOperators_BauschkeCombettes_2017 {H : Type u} : Add (H → ↑(Set.Ioi ⊥))

The canonical source-facing addition on ]-∞,+∞]-valued functions is pointwise addition.

@[implicit_reducible]

noncomputable instance ERealFunction.instAddCommMonoidForallElemERealIoiBot_convexAnalysisMonotoneOperators_BauschkeCombettes_2017 {H : Type u} : AddCommMonoid (H → ↑(Set.Ioi ⊥))

The canonical source-facing additive structure on ]-∞,+∞]-valued functions is pointwise addition.

@[simp]

theorem ERealFunction.zero_apply {H : Type u} (x : H) : ↑(0 x) = 0

Coercing the additive identity of ]-∞,+∞]-valued functions to EReal recovers the constant zero function.

@[simp]

theorem ERealFunction.add_apply {H : Type u} (f g : H → ↑(Set.Ioi ⊥)) (x : H) : ↑((f + g) x) = ↑(f x) + ↑(g x)

Coercing f + g to EReal recovers ordinary pointwise addition.

@[simp]

theorem ERealFunction.sum_apply {H : Type u} {ι : Type v} (s : Finset ι) (f : ι → H → ↑(Set.Ioi ⊥)) (x : H) : ↑((∑ i ∈ s, f i) x) = ∑ i ∈ s, ↑(f i x)

Coercing a finite pointwise sum of ]-∞,+∞]-valued functions to EReal recovers the ordinary finite sum of the coerced values.

def ERealFunction.«term_⊕_» : Lean.TrailingParserDescr

The separable sum of f and g on the product space H × H.

@[simp]

theorem ERealFunction.separableSum_apply {H : Type u} (f g : H → ↑(Set.Ioi ⊥)) (p : H × H) : ↑((fun (f g : H → ↑(Set.Ioi ⊥)) => pointwiseAdd (f ∘ Prod.fst) (g ∘ Prod.snd)) f g p) = ↑(f p.1) + ↑(g p.2)

Coercing f ⊕ g to EReal recovers the separable sum (x, y) ↦ f x + g y.

theorem ERealFunction.mem_effectiveDomain_pointwiseAdd_iff {H : Type u} (f g : H → ↑(Set.Ioi ⊥)) (x : H) : x ∈ effectiveDomain (f + g) ↔ x ∈ effectiveDomain f ∧ x ∈ effectiveDomain g

Helper for Proposition 9.30: the effective domain of the pointwise sum is exactly the intersection of the effective domains of the summands.

theorem ERealFunction.effectiveDomain_add_nonempty_of_inter_nonempty {H : Type u} (f g : H → ↑(Set.Ioi ⊥)) (hdom : (effectiveDomain f ∩ effectiveDomain g).Nonempty) : (effectiveDomain (f + g)).Nonempty

If the effective domains of f and g meet, then the effective domain of f + g is nonempty.

theorem ERealFunction.pointwiseAdd_mem_gammaZero {H : Type u} [TopologicalSpace H] [AddCommGroup H] [Module ℝ H] [SequentialSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] (f g : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) (hg : g ∈ Γ₀(H)) (hdom : (effectiveDomain f ∩ effectiveDomain g).Nonempty) : f + g ∈ Γ₀(H)

The pointwise sum of two members of Γ₀(H) again belongs to Γ₀(H) as soon as their effective domains meet.

theorem ERealFunction.recessionFunction_mem_gammaZero {H : Type u} [TopologicalSpace H] [AddCommGroup H] [Module ℝ H] [SequentialSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) : recessionFunction f ⋯ ∈ Γ₀(H)

Proposition 9.30 (1): clause (i). The recession function of a Γ₀(H) function again belongs to Γ₀(H).

theorem ERealFunction.tendsto_directionalDifferenceQuotient_to_recessionFunction {H : Type u} [TopologicalSpace H] [AddCommGroup H] [Module ℝ H] [SequentialSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) {x : H} (hx : x ∈ effectiveDomain f) (y : H) : Filter.Tendsto (directionalDifferenceQuotient f x y) Filter.atTop (nhds ↑(recessionFunction f ⋯ y))

Proposition 9.30 (2): clause (ii). The recession function is the limit at +∞ of the directional difference quotient along the ray x + α • y.

theorem ERealFunction.tendsto_scaled_ray_values_to_recessionFunction {H : Type u} [TopologicalSpace H] [AddCommGroup H] [Module ℝ H] [SequentialSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) {x : H} (hx : x ∈ effectiveDomain f) (y : H) : Filter.Tendsto (fun (α : ↑(Set.Ioi 0)) => ↑(f (x + ↑α • y)) / ↑↑α) Filter.atTop (nhds ↑(recessionFunction f ⋯ y))

Proposition 9.30 (3): clause (iii). The recession function is also the limit at +∞ of the scaled values f (x + α • y) / α.

theorem ERealFunction.recessionFunction_eq_sSup_directionalDifferenceQuotient {H : Type u} [TopologicalSpace H] [AddCommGroup H] [Module ℝ H] [SequentialSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) {x : H} (hx : x ∈ effectiveDomain f) (y : H) : ↑(recessionFunction f ⋯ y) = sSup (Set.range (directionalDifferenceQuotient f x y))

Proposition 9.30 (4): clause (iv). The recession function equals the supremum of the directional difference quotient over positive scalars.

theorem ERealFunction.recessionFunction_nonneg_of_bddBelow {H : Type u} [TopologicalSpace H] [AddCommGroup H] [Module ℝ H] [SequentialSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] (f : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) (hbounded : ∃ (m : ℝ), ∀ (z : H), ↑m ≤ ↑(f z)) (y : H) : 0 ≤ ↑(recessionFunction f ⋯ y)

Proposition 9.30 (5): clause (v). If f is bounded below, then its recession function is pointwise nonnegative.

theorem ERealFunction.recessionFunction_add {H : Type u} [TopologicalSpace H] [AddCommGroup H] [Module ℝ H] [SequentialSpace H] [IsTopologicalAddGroup H] [ContinuousSMul ℝ H] (f g : H → ↑(Set.Ioi ⊥)) (hf : f ∈ Γ₀(H)) (hg : g ∈ Γ₀(H)) (hdom : (effectiveDomain f ∩ effectiveDomain g).Nonempty) : (fun (y : H) => ↑(recessionFunction (pointwiseAdd f g) ⋯ y)) = fun (y : H) => ↑(recessionFunction f ⋯ y) + ↑(recessionFunction g ⋯ y)

Proposition 9.30 (6): clause (vi). When the effective domains of f and g meet, the recession function of f + g is the pointwise sum of the recession functions.

theorem ERealFunction.effectiveDomain_comp_nonempty_of_range_inter_nonempty {H : Type u} {K : Type v} [SeminormedAddCommGroup H] [NormedSpace ℝ H] [SeminormedAddCommGroup K] [NormedSpace ℝ K] (g : K → ↑(Set.Ioi ⊥)) (L : H →L[ℝ] K) (hdom : (Set.range ⇑L ∩ effectiveDomain g).Nonempty) : (effectiveDomain (g ∘ ⇑L)).Nonempty

If the range of L meets the effective domain of g, then the effective domain of g ∘ L is nonempty.

theorem ERealFunction.recessionFunction_comp_continuousLinearMap {H : Type u} {K : Type v} [SeminormedAddCommGroup H] [NormedSpace ℝ H] [SeminormedAddCommGroup K] [NormedSpace ℝ K] (g : K → ↑(Set.Ioi ⊥)) (hg : g ∈ Γ₀(K)) (L : H →L[ℝ] K) (hdom : (Set.range ⇑L ∩ effectiveDomain g).Nonempty) : (fun (y : H) => ↑(recessionFunction (g ∘ ⇑L) ⋯ y)) = fun (y : H) => ↑(recessionFunction g ⋯ (L y))

Proposition 9.30 (7): clause (vii). Composing with a continuous linear map commutes with the recession function when the range of the map meets the effective domain.