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

Upper quadratic contacts

This file contains the upper-contact predicate used in the Aleksandrov proof route.

def AleksandrovDifferentiability.HasUpperContactWithSlopeOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (x p : E) (a : ℝ) : Prop

u has an upper quadratic contact of opening a and slope p at x, relative to s.

Equations

• AleksandrovDifferentiability.HasUpperContactWithSlopeOn s u x p a = (x ∈ s ∧ ∀ y ∈ s, u y ≤ u x + inner ℝ p (y - x) + a / 2 * ‖y - x‖ ^ 2)

def AleksandrovDifferentiability.HasUpperContactOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (x : E) (a : ℝ) : Prop

u has an upper quadratic contact of opening a at x, relative to s.

The vector p is the slope of the touching quadratic. The definition does not require 0 ≤ a; estimates that use the geometric opening should carry that hypothesis explicitly.

Equations

• AleksandrovDifferentiability.HasUpperContactOn s u x a = ∃ (p : E), AleksandrovDifferentiability.HasUpperContactWithSlopeOn s u x p a

def AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (x : E) (A : ℝ) : Prop

The upper-contact opening is at most A, expressed through the approximation property used in proofs: every larger opening A + η, η > 0, has an upper contact.

Equations

• AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn s u x A = ∀ (η : ℝ), 0 < η → AleksandrovDifferentiability.HasUpperContactOn s u x (A + η)

def AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (x p : E) (A : ℝ) : Prop

Fixed-slope version of HasUpperContactOpeningAtMostOn: every larger opening A + η, η > 0, has an upper contact with the prescribed slope p.

Equations

• AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn s u x p A = ∀ (η : ℝ), 0 < η → AleksandrovDifferentiability.HasUpperContactWithSlopeOn s u x p (A + η)

def AleksandrovDifferentiability.upperContactSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (a : ℝ) : Set E

Points of s where u has an upper quadratic contact of opening a.

Equations

• AleksandrovDifferentiability.upperContactSet s u a = {x : E | AleksandrovDifferentiability.HasUpperContactOn s u x a}

def AleksandrovDifferentiability.upperContactWithSlopeSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (p : E) (a : ℝ) : Set E

Points of s where u has an upper quadratic contact of opening a and slope p.

Equations

• AleksandrovDifferentiability.upperContactWithSlopeSet s u p a = {x : E | AleksandrovDifferentiability.HasUpperContactWithSlopeOn s u x p a}

def AleksandrovDifferentiability.upperContactOpeningAtMostSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (A : ℝ) : Set E

Points of s where the upper-contact opening is at most A.

Equations

• AleksandrovDifferentiability.upperContactOpeningAtMostSet s u A = {x : E | AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn s u x A}

def AleksandrovDifferentiability.upperContactWithSlopeOpeningAtMostSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] (s : Set E) (u : E → ℝ) (p : E) (A : ℝ) : Set E

Points of s where the upper-contact opening is at most A with prescribed slope p.

Equations

• AleksandrovDifferentiability.upperContactWithSlopeOpeningAtMostSet s u p A = {x : E | AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn s u x p A}

@[simp]

theorem AleksandrovDifferentiability.mem_upperContactSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a : ℝ} : x ∈ upperContactSet s u a ↔ HasUpperContactOn s u x a

@[simp]

theorem AleksandrovDifferentiability.mem_upperContactWithSlopeSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {a : ℝ} : x ∈ upperContactWithSlopeSet s u p a ↔ HasUpperContactWithSlopeOn s u x p a

@[simp]

theorem AleksandrovDifferentiability.mem_upperContactOpeningAtMostSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A : ℝ} : x ∈ upperContactOpeningAtMostSet s u A ↔ HasUpperContactOpeningAtMostOn s u x A

@[simp]

theorem AleksandrovDifferentiability.mem_upperContactWithSlopeOpeningAtMostSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {A : ℝ} : x ∈ upperContactWithSlopeOpeningAtMostSet s u p A ↔ HasUpperContactWithSlopeOpeningAtMostOn s u x p A

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.mem {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {a : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) : x ∈ s

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.upper_inequality {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p y : E} {a : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) (hy : y ∈ s) : u y ≤ u x + inner ℝ p (y - x) + a / 2 * ‖y - x‖ ^ 2

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.hasUpperContactOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {a : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) : HasUpperContactOn s u x a

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.mono_opening {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {a b : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) (hab : a ≤ b) : HasUpperContactWithSlopeOn s u x p b

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOn.mono_opening_add_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {a c : ℝ} (h : HasUpperContactWithSlopeOn s u x p a) (hc : 0 ≤ c) : HasUpperContactWithSlopeOn s u x p (a + c)

theorem AleksandrovDifferentiability.HasUpperContactOn.mem {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a : ℝ} (h : HasUpperContactOn s u x a) : x ∈ s

theorem AleksandrovDifferentiability.HasUpperContactOn.exists_slope {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a : ℝ} (h : HasUpperContactOn s u x a) : ∃ (p : E), ∀ y ∈ s, u y ≤ u x + inner ℝ p (y - x) + a / 2 * ‖y - x‖ ^ 2

theorem AleksandrovDifferentiability.HasUpperContactOn.exists_slope_contact {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a : ℝ} (h : HasUpperContactOn s u x a) : ∃ (p : E), HasUpperContactWithSlopeOn s u x p a

theorem AleksandrovDifferentiability.HasUpperContactOn.mono_opening {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a b : ℝ} (h : HasUpperContactOn s u x a) (hab : a ≤ b) : HasUpperContactOn s u x b

theorem AleksandrovDifferentiability.HasUpperContactOn.mono_opening_add_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {a c : ℝ} (h : HasUpperContactOn s u x a) (hc : 0 ≤ c) : HasUpperContactOn s u x (a + c)

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.hasUpperContactOn_add_pos {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A η : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hη : 0 < η) : HasUpperContactOn s u x (A + η)

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.exists_slope_contact_add_pos {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A η : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hη : 0 < η) : ∃ (p : E), HasUpperContactWithSlopeOn s u x p (A + η)

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.mem {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) : x ∈ s

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.mono_bound {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A B : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hAB : A ≤ B) : HasUpperContactOpeningAtMostOn s u x B

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.mono_bound_add_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A c : ℝ} (h : HasUpperContactOpeningAtMostOn s u x A) (hc : 0 ≤ c) : HasUpperContactOpeningAtMostOn s u x (A + c)

theorem AleksandrovDifferentiability.HasUpperContactOpeningAtMostOn.of_hasUpperContactOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x : E} {A : ℝ} (h : HasUpperContactOn s u x A) : HasUpperContactOpeningAtMostOn s u x A

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.hasUpperContactWithSlopeOn_add_pos {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {A η : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hη : 0 < η) : HasUpperContactWithSlopeOn s u x p (A + η)

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.hasUpperContactOpeningAtMostOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {A : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) : HasUpperContactOpeningAtMostOn s u x A

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.mem {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {A : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) : x ∈ s

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.mono_bound {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {A B : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hAB : A ≤ B) : HasUpperContactWithSlopeOpeningAtMostOn s u x p B

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.mono_bound_add_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {A c : ℝ} (h : HasUpperContactWithSlopeOpeningAtMostOn s u x p A) (hc : 0 ≤ c) : HasUpperContactWithSlopeOpeningAtMostOn s u x p (A + c)

theorem AleksandrovDifferentiability.HasUpperContactWithSlopeOpeningAtMostOn.of_hasUpperContactWithSlopeOn {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {x p : E} {A : ℝ} (h : HasUpperContactWithSlopeOn s u x p A) : HasUpperContactWithSlopeOpeningAtMostOn s u x p A

theorem AleksandrovDifferentiability.upperContactWithSlopeSet_subset_upperContactSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {p : E} {a : ℝ} : upperContactWithSlopeSet s u p a ⊆ upperContactSet s u a

theorem AleksandrovDifferentiability.upperContactSet_subset_domain {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {a : ℝ} : upperContactSet s u a ⊆ s

theorem AleksandrovDifferentiability.upperContactWithSlopeSet_subset_domain {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {p : E} {a : ℝ} : upperContactWithSlopeSet s u p a ⊆ s

theorem AleksandrovDifferentiability.upperContactSet_mono_opening {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {a b : ℝ} (hab : a ≤ b) : upperContactSet s u a ⊆ upperContactSet s u b

theorem AleksandrovDifferentiability.upperContactWithSlopeSet_mono_opening {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {p : E} {a b : ℝ} (hab : a ≤ b) : upperContactWithSlopeSet s u p a ⊆ upperContactWithSlopeSet s u p b

theorem AleksandrovDifferentiability.upperContactSet_subset_upperContactOpeningAtMostSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {A : ℝ} : upperContactSet s u A ⊆ upperContactOpeningAtMostSet s u A

theorem AleksandrovDifferentiability.upperContactWithSlopeSet_subset_upperContactWithSlopeOpeningAtMostSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {p : E} {A : ℝ} : upperContactWithSlopeSet s u p A ⊆ upperContactWithSlopeOpeningAtMostSet s u p A

theorem AleksandrovDifferentiability.upperContactWithSlopeOpeningAtMostSet_subset_upperContactOpeningAtMostSet {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {p : E} {A : ℝ} : upperContactWithSlopeOpeningAtMostSet s u p A ⊆ upperContactOpeningAtMostSet s u A

theorem AleksandrovDifferentiability.upperContactOpeningAtMostSet_subset_domain {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {A : ℝ} : upperContactOpeningAtMostSet s u A ⊆ s

theorem AleksandrovDifferentiability.upperContactWithSlopeOpeningAtMostSet_subset_domain {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {p : E} {A : ℝ} : upperContactWithSlopeOpeningAtMostSet s u p A ⊆ s

theorem AleksandrovDifferentiability.upperContactOpeningAtMostSet_mono_bound {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {A B : ℝ} (hAB : A ≤ B) : upperContactOpeningAtMostSet s u A ⊆ upperContactOpeningAtMostSet s u B

theorem AleksandrovDifferentiability.upperContactWithSlopeOpeningAtMostSet_mono_bound {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] {s : Set E} {u : E → ℝ} {p : E} {A B : ℝ} (hAB : A ≤ B) : upperContactWithSlopeOpeningAtMostSet s u p A ⊆ upperContactWithSlopeOpeningAtMostSet s u p B