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

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

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

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

Let u be bounded above on C, and let v be bounded below on C. If, for all i in a set belonging to l, x i ∈ C and y i ∈ C, then there exist 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.

theorem ViscositySolns.eventually_uv_bounds_of_upper_lowerBoundedOn_of_eventually_isMaxOn {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} (hu : ValueUpperBoundedOn C u) (hv : ValueLowerBoundedOn C v) (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 ≤ v (y i) ∧ u (x i) ≤ M

Let u be bounded above on C, and let v be bounded below on C. If (x i, y i) maximizes the doubled-variable objective on C × 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 ≤ v (y i) and u (x i) ≤ M.

theorem ViscositySolns.tendsto_valueGap_zero_of_continuousAt_of_tendsto_same {n : ℕ} {ι : Type u_1} {l : Filter ι} {u : Point n → ℝ} {x y : ι → Point n} {z : Point n} (hu : ContinuousAt u z) (hx : Filter.Tendsto x l (nhds z)) (hy : Filter.Tendsto y l (nhds z)) : Filter.Tendsto (fun (i : ι) => u (x i) - u (y i)) l (nhds 0)

Let u : R^n -> R be continuous at z. If x i -> z and y i -> z along l, then u (x i) - u (y i) -> 0 along l.

theorem ViscositySolns.tendsto_valueGap_zero_of_continuousAt_of_tendsto_pair_diagonal {n : ℕ} {ι : Type u_1} {l : Filter ι} {u : Point n → ℝ} {x y : ι → Point n} {z : Point n} (hu : ContinuousAt u z) (hxy : Filter.Tendsto (fun (i : ι) => (x i, y i)) l (nhds (z, z))) : Filter.Tendsto (fun (i : ι) => u (x i) - u (y i)) l (nhds 0)

Let u : R^n -> R be continuous at z. If (x i, y i) -> (z, z) along l, then u (x i) - u (y i) -> 0 along l.

theorem ViscositySolns.tendsto_right_of_tendsto_left_of_tendsto_distance_zero {n : ℕ} {ι : Type u_1} {l : Filter ι} {x y : ι → Point n} {z : Point n} (hx : Filter.Tendsto x l (nhds z)) (hdist : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)) : Filter.Tendsto y l (nhds z)

If x i -> z and ‖x i - y i‖ -> 0 along l, then y i -> z along l.

theorem ViscositySolns.tendsto_pair_diagonal_of_tendsto_left_of_tendsto_distance_zero {n : ℕ} {ι : Type u_1} {l : Filter ι} {x y : ι → Point n} {z : Point n} (hx : Filter.Tendsto x l (nhds z)) (hdist : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => (x i, y i)) l (nhds (z, z))

If x i -> z and ‖x i - y i‖ -> 0 along l, then (x i, y i) -> (z, z) along l.

theorem ViscositySolns.tendsto_right_nhdsWithin_of_tendsto_left_nhdsWithin_of_tendsto_distance_zero {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {x y : ι → Point n} {z : Point n} (hx : Filter.Tendsto x l (nhdsWithin z C)) (hyC : ∀ᶠ (i : ι) in l, y i ∈ C) (hdist : Filter.Tendsto (fun (i : ι) => ‖x i - y i‖) l (nhds 0)) : Filter.Tendsto y l (nhdsWithin z C)

If x i -> z within C, if y i ∈ C for all i in a set belonging to l, and if ‖x i - y i‖ -> 0 along l, then y i -> z within C along l.

theorem ViscositySolns.tendsto_nhdsWithin_of_tendsto_norm_sub_zero_of_eventually_mem {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {x : ι → Point n} {z : Point n} (hxz : Filter.Tendsto (fun (i : ι) => ‖x i - z‖) l (nhds 0)) (hxC : ∀ᶠ (i : ι) in l, x i ∈ C) : Filter.Tendsto x l (nhdsWithin z C)

If ‖x i - z‖ -> 0 along l and x i ∈ C for all i in a set belonging to l, then x i -> z within C along l.

theorem ViscositySolns.tendsto_valueGap_zero_of_continuousWithinAt_of_tendsto_same {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u : Point n → ℝ} {x y : ι → Point n} {z : Point n} (hu : ContinuousWithinAt u C z) (hx : Filter.Tendsto x l (nhdsWithin z C)) (hy : Filter.Tendsto y l (nhdsWithin z C)) : Filter.Tendsto (fun (i : ι) => u (x i) - u (y i)) l (nhds 0)

Let u : R^n -> R be continuous at z relative to C. If x i -> z within C and y i -> z within C along l, then u (x i) - u (y i) -> 0 along l.

theorem ViscositySolns.eventually_value_sub_lt_of_upper_lowerSemicontinuousWithinAt_of_tendsto_same {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {x y : ι → Point n} {z : Point n} {ε : ℝ} (hu : UpperSemicontinuousWithinAt u C z) (hv : LowerSemicontinuousWithinAt v C z) (hx : Filter.Tendsto x l (nhdsWithin z C)) (hy : Filter.Tendsto y l (nhdsWithin z C)) (hε : 0 < ε) : ∀ᶠ (i : ι) in l, u (x i) - v (y i) < u z - v z + ε

Let u be upper semicontinuous at z relative to C, and let v be lower semicontinuous at z relative to C. If x i -> z within C and y i -> z within C along l, then for every real number ε > 0,

u (x i) - v (y i) < u z - v z + ε

for all i in a set belonging to l.

theorem ViscositySolns.shifted_gap_at_limit_of_closure_maximizers {n : ℕ} {ι : Type u_1} {l : Filter ι} [l.NeBot] {C : Set (Point n)} {u v : Point n → ℝ} {δ : ℝ} {α : ι → ℝ} {x y : ι → Point n} {z x0 : Point n} (hz : z ∈ C) (hgap : v z < u z - δ) (hx0closure : x0 ∈ closure C) (hu : UpperSemicontinuousOn (fun (z : Point n) => u z - δ) (closure C)) (hv : LowerSemicontinuousOn v (closure C)) (hx : Filter.Tendsto x l (nhdsWithin x0 (closure C))) (hy : Filter.Tendsto y l (nhdsWithin x0 (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)) : v x0 < u x0 - δ

Let (x i, y i) maximize the shifted doubled-variable objective on closure C × closure C for all i in a set belonging to l. Suppose z ∈ C, v z < u z - δ, and x0 ∈ closure C. If x i -> x0 and y i -> x0 within closure C, and if x ↦ u x - δ is upper semicontinuous on closure C while v is lower semicontinuous on closure C, then v x0 < u x0 - δ.

theorem ViscositySolns.tendsto_weightedDistanceSq_zero_of_eventually_isMaxOn_of_semicontinuousOn_of_tendsto_same {n : ℕ} {ι : Type u_1} {l : Filter ι} {C : Set (Point n)} {u v : Point n → ℝ} {α : ι → ℝ} {x y : ι → Point n} {z : Point n} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v C) (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)) (hx : Filter.Tendsto x l (nhdsWithin z C)) (hy : Filter.Tendsto y l (nhdsWithin z C)) : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)

Let (x i, y i) maximize the doubled-variable objective on C × C for all i in a set belonging to l. Suppose z ∈ C, u is upper semicontinuous on C, v is lower semicontinuous on C, x i -> z within C, and y i -> z within C, all along l. Then

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

along l.

theorem ViscositySolns.tendsto_weightedDistanceSq_zero_of_shifted_closure_maximizers_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 - δ) (hu : UpperSemicontinuousOn (fun (z : Point n) => u z - δ) (closure C)) (hv : LowerSemicontinuousOn v (closure C)) (hx : Filter.Tendsto x l (nhdsWithin x0 (closure C))) (hy : Filter.Tendsto y l (nhdsWithin x0 (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)) : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)

Assume u ≤ v on frontier C and δ > 0. Suppose x0 ∈ closure C, v x0 < u x0 - δ, x i -> x0 and y i -> x0 within closure C, and (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 x ↦ u x - δ is upper semicontinuous on closure C and v is lower semicontinuous on closure C, then

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

along l.

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

Assume α i * ‖x i - y i‖ ^ 2 -> 0 along l, and assume that 1 ≤ α i for all i in a set belonging to l. Then ‖x i - y i‖ -> 0 along l.

theorem ViscositySolns.tendsto_comparisonScale_zero_of_shifted_closure_maximizers_of_tendsto_atTop {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 - δ) (hu : UpperSemicontinuousOn (fun (z : Point n) => u z - δ) (closure C)) (hv : LowerSemicontinuousOn v (closure C)) (hx : Filter.Tendsto x l (nhdsWithin x0 (closure C))) (hy : Filter.Tendsto y l (nhdsWithin x0 (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)) (hα : Filter.Tendsto α l Filter.atTop) : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2 + ‖x i - y i‖) l (nhds 0)

Under the hypotheses of tendsto_weightedDistanceSq_zero_of_shifted_closure_maximizers_of_tendsto, if additionally α i -> +∞, then

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

along l.

theorem ViscositySolns.doubledVariableScaleEstimatesAlong_of_quadratic_of_eventually_one_le_of_ne {n : ℕ} {ι : Type u_1} {l : Filter ι} {α : ι → ℝ} {x y : ι → Point n} (hquad : Filter.Tendsto (fun (i : ι) => α i * ‖x i - y i‖ ^ 2) l (nhds 0)) (hαone : ∀ᶠ (i : ι) in l, 1 ≤ α i) (hne : ∀ᶠ (i : ι) in l, x i ≠ y i) : DoubledVariableScaleEstimatesAlong l α x y

Assume α i * ‖x i - y i‖ ^ 2 -> 0 along l, assume that 1 ≤ α i for all i in a set belonging to l, and assume that x i ≠ y i for all i in a set belonging to l. Then DoubledVariableScaleEstimatesAlong l α x y holds.

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

Assume α i * ‖x i - y i‖ ^ 2 -> 0 along l, assume α i -> +∞ along l, and assume {i | x i ≠ y i} belongs to l. Then DoubledVariableScaleEstimatesAlong l α x y holds.

theorem ViscositySolns.strictDoubledVariableLocalizationAlongOn_of_eventually_maximizers_of_scalarRange_of_scales {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)) (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)) (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 α i * ‖x i - y i‖ ^ 2 -> 0, if ‖x i - y i‖ -> 0, and if the selected scale is positive for all i in a set belonging to l, then these data satisfy StrictDoubledVariableLocalizationAlongOn C R u v l α x y.

theorem ViscositySolns.strictDoubledVariableLocalizationAlongOn_of_scales_of_ne {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)) (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)) (hne : ∀ᶠ (i : ι) in l, 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 α i * ‖x i - y i‖ ^ 2 -> 0, if ‖x i - y i‖ -> 0, and if x i ≠ y i for all i in a set belonging to l, then these data satisfy StrictDoubledVariableLocalizationAlongOn C R u v l α x y.

theorem ViscositySolns.strictDoubledVariableLocalizationAlongOn_of_scaleEstimates {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 : DoubledVariableScaleEstimatesAlong l α x y) : StrictDoubledVariableLocalizationAlongOn C R u v l α x y

Assume there are functions α : ι -> R and x y : ι -> R^n such that, for all i in a set belonging to l, one has 0 < α i, x i ∈ C, y i ∈ C, and (x i, y i) maximizes (x', y') ↦ u x' - v y' - (α i / 2) * ∑ j, (x' j - y' j)^2 on C × C.

If there exists z ∈ C such that v z < u z, if ScalarRangeOn C R u holds, and if DoubledVariableScaleEstimatesAlong l α x y holds, then StrictDoubledVariableLocalizationAlongOn C R u v l α x y holds.