Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Doubled-variable localization estimates for proper comparison. (SelectedMaximizers)

Part of the doubled-variable localization estimates for proper comparison. Split from Localization.lean; see the umbrella module docstring.

theorem ViscositySolns.eventually_value_right_le_left_of_eventually_isMaxOn_doubledObjective {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hfail : ∃ z ∈ C, v z < u z) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) : ∀ᶠ (i : ι) in l, v (y i) ≤ u (x i)

Let α i, x i, and y i be selected doubled-variable data along a filter l. Suppose there exists z ∈ C such that v z < u z. If, for all i in a set belonging to l, α i > 0, x i ∈ C, y i ∈ C, and (x i, y i) maximizes the doubled-variable objective on C × C, then for all i in a set belonging to l, v (y i) ≤ u (x i).

theorem ViscositySolns.eventually_scalarRange_of_eventually_isMaxOn_doubledObjective {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (huR : ScalarRangeOn C R u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) : ∀ᶠ (i : ι) in l, u (x i) ∈ R

Let α i, x i, and y i be selected doubled-variable data along a filter l. If, for all i in a set belonging to l, x i ∈ C, and if u x ∈ R for every x ∈ C, then for all i in a set belonging to l, u (x i) ∈ R.

theorem ViscositySolns.eventually_isMaxOn_doubledObjective_restrict_closure {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ closure C ∧ y i ∈ closure C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (closure C ×ˢ closure C) (x i, y i)) (hmem : ∀ᶠ (i : ι) in l, x i ∈ C ∧ y i ∈ C) : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)

Suppose (x i, y i) maximizes the doubled-variable objective on closure C × closure C for all i in a set belonging to l. If x i ∈ C and y i ∈ C for all i in a set belonging to l, then (x i, y i) maximizes the same objective on C × C for all i in a set belonging to l.

theorem ViscositySolns.eventually_isMaxOn_shifted_doubledObjective_restrict_closure_of_tendsto {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {δ : ℝ} {α : ι → ℝ} {x y : ι → Point n} {x0 : Point n} (hboundary : BoundaryComparisonOn C u v) (hδ : 0 < δ) (hx0closure : x0 ∈ closure C) (hgap : v x0 < u x0 - δ) (hx : Filter.Tendsto x l (nhds x0)) (hy : Filter.Tendsto y l (nhds x0)) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ closure C ∧ y i ∈ closure C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective (fun (z : Point n) => u z - δ) v (α i) q) (closure C ×ˢ closure C) (x i, y i)) : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective (fun (z : Point n) => u z - δ) v (α i) q) (C ×ˢ C) (x i, y i)

Assume u ≤ v on frontier C and δ > 0. Suppose x0 ∈ closure C, v x0 < u x0 - δ, x i -> x0, and y i -> x0. If (x i, y i) maximizes

(x', y') ↦ u x' - δ - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2

on closure C × closure C for all i in a set belonging to l, then (x i, y i) maximizes the same function on C × C for all i in a set belonging to l.

theorem ViscositySolns.eventually_shifted_value_sub_ge_of_closure_maximizers {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {δ : ℝ} {α : ι → ℝ} {x y : ι → Point n} {z : Point n} (hz : z ∈ closure C) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ closure C ∧ y i ∈ closure C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective (fun (z : Point n) => u z - δ) v (α i) q) (closure C ×ˢ closure C) (x i, y i)) : ∀ᶠ (i : ι) in l, u z - δ - v z ≤ u (x i) - δ - v (y i)

Suppose (x i, y i) maximizes the shifted doubled-variable objective on closure C × closure C for all i in a set belonging to l. If z ∈ closure C, then, for all i in a set belonging to l,

u z - δ - v z ≤ u (x i) - δ - v (y i).

theorem ViscositySolns.strictDoubledVariableLocalizationAlongOn_of_shifted_closure_maximizers_of_tendsto {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} {δ : ℝ} {α : ι → ℝ} {x y : ι → Point n} {x0 : Point n} (hboundary : BoundaryComparisonOn C u v) (hδ : 0 < δ) (hx0closure : x0 ∈ closure C) (hgap : v x0 < u x0 - δ) (hx : Filter.Tendsto x l (nhds x0)) (hy : Filter.Tendsto y l (nhds x0)) (huR : ScalarRangeOn C R fun (z : Point n) => u z - δ) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ closure C ∧ y i ∈ closure C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective (fun (z : Point n) => u z - δ) v (α i) q) (closure C ×ˢ closure C) (x i, y i)) (hscale : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) l (nhdsWithin 0 (Set.Ioi 0))) : StrictDoubledVariableLocalizationAlongOn C R (fun (z : Point n) => u z - δ) v l α x y

Assume u ≤ v on frontier C and δ > 0. Suppose x0 ∈ closure C, v x0 < u x0 - δ, x i -> x0, and y i -> x0. Suppose also that, for all i in a set belonging to l, (x i, y i) maximizes

(x', y') ↦ u x' - δ - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2

on closure C × closure C. If the shifted function x ↦ u x - δ has values in R on C, and if

α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖

tends to 0 through positive values along l, then the selected data satisfy StrictDoubledVariableLocalizationAlongOn C R (fun z => u z - δ) v l α x y.

theorem ViscositySolns.ValueBoundedOn.eventually_selected_bounds_of_eventually_mem {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u : Point n → ℝ} {x y : ι → Point n} (hu : ValueBoundedOn C u) (hmem : ∀ᶠ (i : ι) in l, x i ∈ C ∧ y i ∈ C) : ∃ (m : ℝ) (M : ℝ), ∀ᶠ (i : ι) in l, m ≤ u (y i) ∧ u (x i) ≤ M

Let u be bounded on C, and let x i and y i belong to C for all i in a set belonging to l. Then there exist real numbers m and M such that, for all i in a set belonging to l, m ≤ u (y i) and u (x i) ≤ M.

theorem ViscositySolns.ValueBoundedOn.eventually_selected_bounds_of_eventually_isMaxOn {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hu : ValueBoundedOn C u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) : ∃ (m : ℝ) (M : ℝ), ∀ᶠ (i : ι) in l, m ≤ u (y i) ∧ u (x i) ≤ M

Let u be bounded on C. If, for all i in a set belonging to l, x i and y i belong to C and (x i, y i) maximizes the doubled-variable objective on C × C, then there exist real numbers m and M such that, for all i in a set belonging to l, m ≤ u (y i) and u (x i) ≤ M.

theorem ViscositySolns.tendsto_nhdsWithin_Ioi_of_tendsto_nhds_of_eventually_pos {ι : Type u_1} {l : Filter ι} {s : ι → ℝ} (hzero : Filter.Tendsto s l (nhds 0)) (hpos : ∀ᶠ (i : ι) in l, 0 < s i) : Filter.Tendsto s l (nhdsWithin 0 (Set.Ioi 0))

Let s i be real numbers. If s i -> 0 along l and 0 < s i for all i in a set belonging to l, then s i -> 0 through positive values along l.

theorem ViscositySolns.eventually_comparisonScale_pos_of_eventually_isMaxOn_of_eventually_ne {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hne : ∀ᶠ (i : ι) in l, x i ≠ y i) : ∀ᶠ (i : ι) in l, 0 < α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖

Let α i, x i, and y i be selected doubled-variable data along a filter l. If, for all i in a set belonging to l, α i > 0, and if x i ≠ y i for all i in a set belonging to l, then for all i in a set belonging to l,

0 < α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖.

theorem ViscositySolns.strictDoubledVariableLocalizationAlongOn_of_eventually_maximizers {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hrange : ∀ᶠ (i : ι) in l, u (x i) ∈ R) (hvyux : ∀ᶠ (i : ι) in l, v (y i) ≤ u (x i)) (hscale : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) l (nhdsWithin 0 (Set.Ioi 0))) : StrictDoubledVariableLocalizationAlongOn C R u v l α x y

Suppose α i, x i, and y i are selected doubled-variable data along a filter l. If, for all i in a set belonging to l, α i > 0, x i ∈ C, y i ∈ C, and (x i, y i) maximizes the doubled-variable objective on C × C; if u (x i) ∈ R and v (y i) ≤ u (x i) also hold for all i in a set belonging to l; and if

α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖

tends to 0 through positive values along l; then StrictDoubledVariableLocalizationAlongOn C R u v l α x y holds.

theorem ViscositySolns.strictDoubledVariableLocalizationAlongOn_of_eventually_maximizers_of_scalarRange {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hfail : ∃ z ∈ C, v z < u z) (huR : ScalarRangeOn C R u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hscale : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) l (nhdsWithin 0 (Set.Ioi 0))) : StrictDoubledVariableLocalizationAlongOn C R u v l α x y

Suppose selected doubled-variable maximizers are available along a filter l, and suppose the associated scales tend to 0 through positive values along l. If there exists z ∈ C such that v z < u z, and if u x ∈ R for every x ∈ C, then these selected data satisfy StrictDoubledVariableLocalizationAlongOn C R u v l α x y.

theorem ViscositySolns.strictDoubledVariableLocalizationAlongOn_of_eventually_maximizers_of_scalarRange_of_scale {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {R : Set ℝ} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hfail : ∃ z ∈ C, v z < u z) (huR : ScalarRangeOn C R u) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hscale_zero : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) l (nhds 0)) (hscale_pos : ∀ᶠ (i : ι) in l, 0 < α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) : StrictDoubledVariableLocalizationAlongOn C R u v l α x y

Suppose selected doubled-variable maximizers are available along a filter l. If there exists z ∈ C such that v z < u z, if ScalarRangeOn C R u holds, if the selected scales tend to 0 along l, and if the selected scales are positive for all i in a set belonging to l, then these data satisfy StrictDoubledVariableLocalizationAlongOn C R u v l α x y.

theorem ViscositySolns.tendsto_comparisonScale_zero_of_tendsto_quadratic_and_distance {n : ℕ} {ι : Type u_1} {l : Filter ι} {α : ι → ℝ} {x y : ι → Point n} (hquad : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)) (hdist : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) l (nhds 0)

If

α i * ‖x i - y i‖ ^ 2 -> 0

and

‖x i - y i‖ -> 0

along l, then the comparison scale

α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖

tends to 0 along l.

theorem ViscositySolns.tendsto_zero_of_eventually_nonneg_of_eventually_le_two_mul_of_tendsto_zero {ι : Type u_1} {l : Filter ι} {s e : ι → ℝ} (hs_nonneg : ∀ᶠ (i : ι) in l, 0 ≤ s i) (hs_le : ∀ᶠ (i : ι) in l, s i ≤ 2 * e i) (he : Filter.Tendsto e l (nhds 0)) : Filter.Tendsto s l (nhds 0)

Let s i and e i be real-valued functions on an index type with filter l. If s i ≥ 0 for all i in a set belonging to l, if s i ≤ 2 * e i for all i in a set belonging to l, and if e i -> 0 along l, then s i -> 0 along l.

theorem ViscositySolns.tendsto_weightedDistanceSq_zero_of_eventually_isMaxOn_of_tendsto_valueGap {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hgap : Filter.Tendsto (fun (i : ι) => u (x i) - u (y i)) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)

Assume (x i, y i) maximizes the doubled-variable objective on C × C for all i in a set belonging to l, and assume u (x i) - u (y i) -> 0 along l. Then α i * ‖x i - y i‖ ^ 2 -> 0 along l.

theorem ViscositySolns.tendsto_distance_zero_of_eventually_weightedDistanceSq_le_const_of_tendsto_atTop {n : ℕ} {ι : Type u_1} {l : Filter ι} {α : ι → ℝ} {x y : ι → Point n} {B : ℝ} (hα : Filter.Tendsto α l Filter.atTop) (hle : ∀ᶠ (i : ι) in l, α i * ‖x i - y i‖ ^ 2 ≤ B) : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)

Let α i, x i, and y i be indexed by a filter l. If α i -> +∞ along l and, for all i in a set belonging to l,

α i * ‖x i - y i‖ ^ 2 ≤ B,

where B is a fixed real number, then ‖x i - y i‖ -> 0 along l.

theorem ViscositySolns.eventually_weightedDistanceSq_le_two_value_range_of_eventually_isMaxOn {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} {m M : ℝ} (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hbounds : ∀ᶠ (i : ι) in l, m ≤ u (y i) ∧ u (x i) ≤ M) : ∀ᶠ (i : ι) in l, α i * ‖x i - y i‖ ^ 2 ≤ 2 * (M - m)

Assume (x i, y i) maximizes the doubled-variable objective on C × C for all i in a set belonging to l. Assume also that, for all i in a set belonging to l, m ≤ u (y i) and u (x i) ≤ M. Then, for all i in a set belonging to l,

α i * ‖x i - y i‖ ^ 2 ≤ 2 * (M - m).

theorem ViscositySolns.tendsto_distance_zero_of_eventually_isMaxOn_of_tendsto_atTop_of_value_bounds {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} {m M : ℝ} (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hα : Filter.Tendsto α l Filter.atTop) (hbounds : ∀ᶠ (i : ι) in l, m ≤ u (y i) ∧ u (x i) ≤ M) : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)

Assume (x i, y i) maximizes the doubled-variable objective on C × C for all i in a set belonging to l. If α i -> +∞ along l and, for all i in a set belonging to l, m ≤ u (y i) and u (x i) ≤ M, then ‖x i - y i‖ -> 0 along l.

theorem ViscositySolns.eventually_weightedDistanceSq_le_two_value_sub_value_at_diagonal_range_of_eventually_isMaxOn {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} {z : Point n} {m M : ℝ} (hz : z ∈ C) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hbounds : ∀ᶠ (i : ι) in l, m ≤ v (y i) ∧ u (x i) ≤ M) : ∀ᶠ (i : ι) in l, α i * ‖x i - y i‖ ^ 2 ≤ 2 * (M - m - (u z - v z))

Assume (x i, y i) maximizes the doubled-variable objective on C × C for all i in a set belonging to l. Suppose z ∈ C, and suppose there are real numbers m and M such that, for all i in a set belonging to l, m ≤ v (y i) and u (x i) ≤ M. Then, for all i in a set belonging to l,

α i * ‖x i - y i‖ ^ 2 ≤ 2 * (M - m - (u z - v z)).

theorem ViscositySolns.tendsto_distance_zero_of_eventually_isMaxOn_of_tendsto_atTop_of_uv_bounds {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} {z : Point n} {m M : ℝ} (hz : z ∈ C) (hmax : ∀ᶠ (i : ι) in l, 0 < α i ∧ x i ∈ C ∧ y i ∈ C ∧ IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v (α i) q) (C ×ˢ C) (x i, y i)) (hα : Filter.Tendsto α l Filter.atTop) (hbounds : ∀ᶠ (i : ι) in l, m ≤ v (y i) ∧ u (x i) ≤ M) : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)

Assume (x i, y i) maximizes the doubled-variable objective on C × C for all i in a set belonging to l. If α i -> +∞ along l, z ∈ C, and there are real numbers m and M such that, for all i in a set belonging to l, m ≤ v (y i) and u (x i) ≤ M, then ‖x i - y i‖ -> 0 along l.