convex analysis: tangentConeAt frontier of a convex set

Stream: Is there code for X?

[Matteo Cipollina]

Does anyone have a clue to how prove that the tangent cone at a frontier point of a convex set
with a non-empty interior is a closed half-space, and if any API around to leverage? In particular I suspect the reverse inclusion, `{d | 0 ≤ ⟪d, -u⟫_ℝ} ⊆ tangentConeAt ℝ s x may requiressome non-trivial (and apparently not available in mathlib or other repositories I've checked) prerequisites.
Thanks in advance :)

import Mathlib

open Set InnerProductSpace RealInnerProductSpace

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]

/-- The tangent cone at a frontier point of a convex set
with a non-empty interior is a closed half-space. The normal of the half-space corresponds
to the normal of a supporting hyperplane at that point. -/
theorem tangentConeAt_frontier_is_halfspace
    (s : Set E) (hs : Convex ℝ s) (hint : (interior s).Nonempty)
    (x : E) (hx : x ∈ frontier s) :
    ∃ u : E, u ≠ 0 ∧ tangentConeAt ℝ s x = {d : E | 0 ≤ ⟪d, u⟫_ℝ} := by
  sorry

[Yaël Dillies]

Is this true? What if s is a square and x one of its vertices? Isn't the tangent cone three quarters of the plane then?

[Yaël Dillies]

docs#tangentConeAt

[Yaël Dillies]

Sorry I confused with the def recently added by @Attila Gáspár, but you can adapt my counterexample: take an arbitrary convex cone with nonempty interior at the origin. Then its tangent cone is itself. But not all such cones are halfspaces

[Yaël Dillies]

What's true is that such tangent cone is contained in a halfspace, and that's easy to prove: just pick any u not in C and argue by convexity

[Yaël Dillies]

And then nonempty interior doesn't help

[Matteo Cipollina]

oh yes, thanks. Am I wrong to think that it holds only assuming smooth boundary points, where the supporting hyperplane is unique?
I've forgot to provide the wider context of this formalization, where this assumption is effectively an axiom (I'm trying to formalize Lieb-Yngvason theormodynamics axiomatic framework). Here, I have assumed an axiom (S2) that provides a so called pressure_map for each state X, which defines a single supporting hyperplane for the forward sector. So I think for my use case, with these assumptions this theorem should hold.

[Matteo Cipollina]

https://github.com/or4nge19/ThermodynamicsLean/blob/main/LY/Axioms.lean

The axiom I'm referring to is S2

namespace LY

universe u v

variable {System : Type u} [TW : ThermoWorld System]

local infix:50 " ≺ " => TW.le
local notation:50 X " ≈ " Y => X ≺ Y ∧ Y ≺ X
local infixr:70 " ⊗ " => TW.comp
local infixr:80 " • " => TW.scale

abbrev SimpleSystemSpace (n : ℕ) := EuclideanSpace ℝ (Fin (n+1))
instance (n:ℕ) : AddCommGroup (SimpleSystemSpace n) := by infer_instance
noncomputable instance (n:ℕ) : Module ℝ (SimpleSystemSpace n) := by infer_instance
instance (n:ℕ) : TopologicalSpace (SimpleSystemSpace n) := by infer_instance

instance (n:ℕ) : Inhabited (SimpleSystemSpace n) := ⟨0⟩

/--
The `IsSimpleSystem` structure holds the data for a single simple system: its identification
with a convex, open subset of a coordinate space. It contains no axioms itself.
-/
structure IsSimpleSystem (n : ℕ) (Γ : System) where
  space : Set (SimpleSystemSpace n)
  isOpen : IsOpen space
  isConvex : Convex ℝ space
  state_equiv : TW.State Γ ≃ Subtype space

/--
A `SimpleSystemFamily` is a collection of systems that are all simple systems of the
same dimension `n`. This class contains the axioms (A7, S1) and the coherence
axioms that govern how simple systems behave under scaling and composition.
-/
class SimpleSystemFamily (n : ℕ) (is_in_family : System → Prop) where
  /-- Provides the `IsSimpleSystem` data structure for any system in the family. -/
  get_ss_inst (Γ : System) (h_in : is_in_family Γ) : IsSimpleSystem n Γ
  /-- The family is closed under positive scaling. -/
  scale_family_closed {Γ} (h_in : is_in_family Γ) {t : ℝ} (ht : 0 < t) :
    is_in_family (t • Γ)

  /-- **Coherence of Scaling and Coordinates (CSS)**: The coordinate map of the scaled
  system `t•Γ` applied to the abstractly scaled state `t•X` yields exactly the
  scalar product of `t` and the coordinates of `X`. This allows to connect abstract system
  algebra and concrete coordinate vector algebra. -/
  coord_of_scaled_state_eq_smul_coord {Γ} (h_in : is_in_family Γ) (X : TW.State Γ) {t : ℝ} (ht : 0 < t) :
    let ss_Γ := get_ss_inst Γ h_in
    let ss_tΓ := get_ss_inst (t • Γ) (scale_family_closed h_in ht)
    ss_tΓ.state_equiv (scale_state ht.ne' X) = t • (ss_Γ.state_equiv X).val

  /-- **A7 (Convex Combination)**: The state formed by composing two scaled-down simple
      systems is adiabatically accessible to the state corresponding to the convex
      combination of their coordinates. -/
  A7 {Γ} (h_in : is_in_family Γ) (X Y : TW.State Γ) {t : ℝ} (ht : 0 < t ∧ t < 1) :
    let ss := get_ss_inst Γ h_in
    let combo_state := comp_state (scale_state ht.1.ne' X, scale_state (sub_pos.mpr ht.2).ne' Y)
    let target_coord_val := t • (ss.state_equiv X).val + (1-t) • (ss.state_equiv Y).val
    have h_target_in_space : target_coord_val ∈ ss.space :=
      ss.isConvex (ss.state_equiv X).property (ss.state_equiv Y).property (le_of_lt ht.1) (le_of_lt (sub_pos.mpr ht.2)) (by ring)
    let target_state : TW.State Γ := ss.state_equiv.symm ⟨target_coord_val, h_target_in_space⟩
    TW.le combo_state target_state

  /-- **S1 (Irreversibility)**: For any state in a simple system, there exists another
      state that is strictly adiabatically accessible from it. -/
  S1 {Γ} (h_in : is_in_family Γ) (X : TW.State Γ) :
    ∃ Y : TW.State Γ, X ≺ Y ∧ ¬ (Y ≺ X)
  pressure_map {Γ} (h_in : is_in_family Γ) : TW.State Γ → EuclideanSpace ℝ (Fin n)
  S2_support_plane {Γ : System} (h_in : is_in_family Γ) (X Y : TW.State Γ) :
    let ss := get_ss_inst Γ h_in
    let P : EuclideanSpace ℝ (Fin n) := pressure_map h_in X
    -- build a EuclideanSpace vector by converting `P` to a function and back
    let normal : SimpleSystemSpace n :=
      WithLp.toLp 2 (Fin.cons (1 : ℝ) (WithLp.ofLp P))
    (X ≺ Y) ↔
      (0 : ℝ) ≤ inner (𝕜 := ℝ) ((ss.state_equiv Y).val - (ss.state_equiv X).val) normal
  /-- **S2 Coherence**: Adiabatically equivalent states have the same pressure map.
      This ensures that the supporting hyperplanes for their forward sectors are parallel. -/
  S2_Coherence {Γ} (h_in : is_in_family Γ) {X Y : TW.State Γ} (h_equiv : X ≈ Y) :
    pressure_map h_in X = pressure_map h_in Y
  /-- **S3 (Connectedness of the Boundary)**: the boundary of the forward sector is path connected. -/
  S3_path_connected {Γ : System} (h_in : is_in_family Γ) (X : TW.State Γ) :
    let ss : IsSimpleSystem n Γ := get_ss_inst Γ h_in
    let coord_sector : Set (SimpleSystemSpace n) :=
      Set.image (fun (Y : TW.State Γ) => (ss.state_equiv Y).val) { Y | X ≺ Y }
    let boundary : Set (SimpleSystemSpace n) := frontier coord_sector
    let adia_points : Set (SimpleSystemSpace n) :=
      { p | p ∈ boundary ∧ ∃ Y : TW.State Γ, (ss.state_equiv Y).val = p ∧ X ≈ Y }
    IsPathConnected adia_points

[Yaël Dillies]

That is still wrong, yes. The tangent cone of the filled parabola $\{(x, y) | y \ge x^2\}$ at $0$ is the upper y-axis. Nevermind, I am confusing with the asymptotic cone again. Your new statement is true

[Yaël Dillies]

Do you still need help proving it?

[Yaël Dillies]

Also your docstrings are misleading: They say things happen in dimension n but, reading your definition of SimpleSystemSpace, they actually happen in dimension n + 1

[Matteo Cipollina]

Yaël Dillies ha scritto:

Do you still need help proving it?

Indeed yes, I'd much appreciate help in proving it as I'm not much familiar with the API and the underlying theory, if not too time consuming :)

Thanks for the correction, yes it was misleading. Indeed identifying the right minimal axioms trying to remain faithful proved to be (unsurprisingly) very hard, this is my 3rd attempt :sweat_smile:

[Yaël Dillies]

Sorry, I am not at a computer anymore, but here are my thoughts. I can't quite make out where the unique hyperplane condition is encoded within your big structure, so I will not talk about it.

[Yaël Dillies]

Sorry, I just realised your statement is wrong again because tangentConeAt is a not necessarily convex cone

[Yaël Dillies]

If you take the convex hull around it, then it should finally be fine

[Yaël Dillies]

Oh, except s is convex, therefore so is the tangent cone

[Yaël Dillies]

I am unclear what exactly you're assuming now. Are you assuming there exists a unique hyperplane supporting x, or at most one?

[Yaël Dillies]

If the former, then you can do it very easily using cone duality:

1. You prove that the dual cone of the tangent cone is the same thing as the dual cone of s.
2. Dualising everything you want that if there exists a unique ray contained in a cone then that cone is that ray, which is obvious.

[Yaël Dillies]

If the latter, then you furthermore need to prove that a supporting hyperplane exists from the fact that your point is on the boundary

[Matteo Cipollina]

Yaël Dillies ha scritto:

I am unclear what exactly you're assuming now. Are you assuming there exists a unique hyperplane supporting x, or at most one?

I am assuming exactly one exists, the S2 axiom (in LY) is both an existence and uniqueness statement: "For each X ∈ Γ the forward sector AX has a unique support plane at X".
S2 is tricky and I have temporarily postulated the half-space geometry directly, which is a much stronger axiom but I thought it gets to the same geometric picture more quickly.
LY actually assume a  weaker S2 (unique hyperplane) and prove the tangent cone is a half-space with a complex argument, basically (if I understand it correctly): if the forward sector Aₓ were 'flat' (withan empty interior), then one could construct infinitely many different supporting hyperplanes for it, which would violate the S2 axiom' that exists a unique supporting hyperplane. The argument is complex but to summarize the tangent cone must be a half-space by showing that any other possibility (a cone smaller than a half-space, which would imply an empty interior for the forward sector) leads to a contradiction with their axioms.
This proof is spread across pag. 39-44 in the paper https://arxiv.org/pdf/cond-mat/9708200

[Yaël Dillies]

Do you have a quick explanation of what the forward sector is?

[Yury G. Kudryashov]

Can you formulate the theorem you want to prove in Lean?

[Matteo Cipollina]

Yaël Dillies ha scritto:

Do you have a quick explanation of what the forward sector is?

sure:
Screenshot 2025-10-18 at 22.51.12.png

[Matteo Cipollina]

Yury G. Kudryashov ha scritto:

Can you formulate the theorem you want to prove in Lean?

Well, after Yael's help, and abstracting from the thermodynamics context, I think what I need to prove is a theorem about the tangent cone of a set that is defined as the intersection of an open set and a closed half-space like this:

import Mathlib.Analysis.Calculus.TangentCone
import Mathlib.Analysis.InnerProductSpace.Basic

open Set InnerProductSpace RealInnerProductSpace

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/--
If a set `s` is the intersection of an open set `U` and a closed half-space `H`,
then the tangent cone to `s` at a point `y` that lies in `U` and on the boundary
of `H` is the half-space `H` translated to the origin.
-/
theorem tangentConeAt_of_intersection_open_with_halfspace
    -- Let U be an open set.
    (U : Set E) (hU : IsOpen U)
    -- Let n be the normal vector defining the half-space.
    (n : E) (hn : n ≠ 0)
    -- Let y be a point on the boundary of the half-space.
    (y : E) (hy_on_boundary : ⟪y, n⟫ = 0)
    -- Assume y is in the open set U.
    (hy_in_U : y ∈ U) :
    -- Let s be the intersection.
    let s := U ∩ {z | ⟪z, n⟫ ≥ 0}
    -- Then the tangent cone at y is the half-space.
    tangentConeAt ℝ s y = {d | ⟪d, n⟫ ≥ 0} := by
  sorry

[Yury G. Kudryashov]

See docs#tangentConeAt_inter_nhds to get rid of U.

[Matteo Cipollina]

Yury G. Kudryashov ha scritto:

See docs#tangentConeAt_inter_nhds to get rid of U.

Thanks! So this would simplify it to this:

import Mathlib.Analysis.Calculus.TangentCone
import Mathlib.Analysis.InnerProductSpace.Basic

open Set InnerProductSpace RealInnerProductSpace

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/-- The tangent cone to a closed half-space at a point on its boundary is the
    half-space itself (translated to the origin). -/
theorem tangentConeAt_halfspace
    -- Let n be the normal vector defining the half-space.
    (n : E) (hn : n ≠ 0)
    -- Let y be a point on the boundary of the half-space.
    (y : E) (hy_on_boundary : ⟪y, n⟫ = 0) :
    -- Let H be the half-space.
    let H := {z | ⟪z, n⟫ ≥ 0}
    -- Then the tangent cone at y is the half-space translated to the origin.
    tangentConeAt ℝ H y = {d | ⟪d, n⟫ ≥ 0} := by
  sorry

[Yury G. Kudryashov]

I think you're looking for docs#posTangentConeAt

[Yaël Dillies]

Up to translation, you can assume y = 0. I'll try proving this tomorrow if you don't get to it before me

[Yury G. Kudryashov]

Here is a slightly cleaned up proof from https://aristotle.harmonic.fun:

theorem posTangentConeAt_of_intersection_open_with_halfspace
    (U : Set E) (hU : IsOpen U)
    (n : E)
    (y : E) (hy_on_boundary : ⟪y, n⟫ = 0)
    (hy_in_U : y ∈ U) :
    posTangentConeAt (U ∩ {z | ⟪z, n⟫ ≥ 0}) y = {d | ⟪d, n⟫ ≥ 0} := by
  refine' Set.Subset.antisymm _ _ <;> intro d hd <;> erw [ posTangentConeAt ] at * <;> simp_all
  · obtain ⟨w, h⟩ := hd
    obtain ⟨w_1, h⟩ := h
    obtain ⟨left, right⟩ := h
    obtain ⟨w_2, h⟩ := left
    obtain ⟨left, right⟩ := right
    -- By the continuity of the inner product, we have ⟪d, n⟫ = lim_{j → ∞} ⟪w_j • w_1 j, n⟫.
    have h_cont : Filter.Tendsto (fun j => ⟪w j • w_1 j, n⟫) Filter.atTop (nhds (⟪d, n⟫)) := by
      exact Filter.Tendsto.inner right tendsto_const_nhds;
    -- Since ⟪y + w_1 j, n⟫ ≥ 0 for all j ≥ w_2, and ⟪y, n⟫ = 0, it follows that ⟪w_1 j, n⟫ ≥ 0 for all j ≥ w_2.
    have h_nonneg : ∀ j ≥ w_2, ⟪w_1 j, n⟫ ≥ 0 := by
      intro j hj; specialize h j hj; simp_all +decide [ inner_add_left ] ;
    -- Since $w_j$ tends to infinity, for sufficiently large $j$, $w_j$ is positive. Therefore, for $j \geq w_2$ and sufficiently large, $⟪w_j • w_1 j, n⟫$ is non-negative.
    have h_pos : ∀ᶠ j in Filter.atTop, 0 ≤ ⟪w j • w_1 j, n⟫ := by
      filter_upwards [ left.eventually_gt_atTop 0, Filter.eventually_ge_atTop w_2 ] with j hj₁ hj₂ using by simpa only [ inner_smul_left ] using mul_nonneg hj₁.le ( h_nonneg j hj₂ ) ;
    exact le_of_tendsto_of_tendsto tendsto_const_nhds h_cont ( by filter_upwards [ h_pos ] with j hj; exact hj );
  · -- Choose $c_n = n$ and $d_n = \frac{1}{n} d$.
    use fun n => n, fun n => (1 / n : ℝ) • d;
    -- Show that the sequence $y + \frac{1}{n} d$ converges to $y$ and is eventually in $U$.
    have h_seq_conv : Filter.Tendsto (fun n : ℕ => y + (1 / (n : ℝ)) • d) Filter.atTop (nhds y) := by
      simpa using tendsto_const_nhds.add ( tendsto_inverse_atTop_nhds_zero_nat.smul_const d );
    exact ⟨ Filter.eventually_atTop.mp ( h_seq_conv.eventually ( hU.mem_nhds hy_in_U ) ) |> fun ⟨ N, hN ⟩ => ⟨ N, fun n hn => ⟨ hN n hn, by simpa [ inner_add_left, inner_smul_left, hy_on_boundary ] using mul_nonneg ( inv_nonneg.2 ( Nat.cast_nonneg _ ) ) hd ⟩ ⟩, tendsto_natCast_atTop_atTop, tendsto_const_nhds.congr' <| by filter_upwards [ Filter.eventually_ne_atTop 0 ] with n hn; simp +decide [ hn ] ⟩

[Yury G. Kudryashov]

I replaced a non-terminal aesop with the output of aesop? and removed an unused argument to simp_all to silence the linters.

[Yury G. Kudryashov]

Of course, this proof can use more cleanup - Aristotle aims to close the goal, not to adhere to the Mathlib style guide.

[Yury G. Kudryashov]

@Yaël Dillies Please don't expand the API about posTangentConeAt. I'm going to redefine tangentConeAt so that posTangentConeAt becones tangentConeAt NNReal.

[Matteo Cipollina]

Yury G. Kudryashov ha scritto:

Here is a slightly cleaned up proof from https://aristotle.harmonic.fun:

Thank you very much :) . Here is also the more general version, dropping U/intersection. Edit: I've seen your last message only now asking not to, but it may still help me (for me) to develop these (now that it seems all much clearer) for my current use while waiting for your generalization:

import Mathlib

open Set Filter Topology InnerProductSpace RealInnerProductSpace
open scoped Topology

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

/--
If a set `s` is the intersection of an open set `U` and a closed half-space `H`,
then the tangent cone to `s` at a point `y` that lies in `U` and on the boundary
of `H` is the half-space `H` translated to the origin. YK
-/
theorem posTangentConeAt_of_intersection_open_with_halfspace'
    (U : Set E) (hU : IsOpen U)
    (n : E)
    (y : E) (hy_on_boundary : ⟪y, n⟫ = 0)
    (hy_in_U : y ∈ U) :
    posTangentConeAt (U ∩ {z | ⟪z, n⟫ ≥ 0}) y = {d | ⟪d, n⟫ ≥ 0} := by
  refine' Set.Subset.antisymm _ _ <;> intro d hd <;> erw [ posTangentConeAt ] at * <;> simp_all
  · obtain ⟨w, h⟩ := hd
    obtain ⟨w_1, h⟩ := h
    obtain ⟨left, right⟩ := h
    obtain ⟨w_2, h⟩ := left
    obtain ⟨left, right⟩ := right
    -- By the continuity of the inner product, we have ⟪d, n⟫ = lim_{j → ∞} ⟪w_j • w_1 j, n⟫.
    have h_cont : Filter.Tendsto (fun j => ⟪w j • w_1 j, n⟫) Filter.atTop (nhds (⟪d, n⟫)) := by
      exact Filter.Tendsto.inner right tendsto_const_nhds;
    -- Since ⟪y + w_1 j, n⟫ ≥ 0 for all j ≥ w_2, and ⟪y, n⟫ = 0, it follows that ⟪w_1 j, n⟫ ≥ 0 for all j ≥ w_2.
    have h_nonneg : ∀ j ≥ w_2, ⟪w_1 j, n⟫ ≥ 0 := by
      intro j hj; specialize h j hj; simp_all +decide [ inner_add_left ] ;
    -- Since $w_j$ tends to infinity, for sufficiently large $j$, $w_j$ is positive. Therefore, for $j \geq w_2$ and sufficiently large, $⟪w_j • w_1 j, n⟫$ is non-negative.
    have h_pos : ∀ᶠ j in Filter.atTop, 0 ≤ ⟪w j • w_1 j, n⟫ := by
      filter_upwards [ left.eventually_gt_atTop 0, Filter.eventually_ge_atTop w_2 ] with j hj₁ hj₂ using by simpa only [ inner_smul_left ] using mul_nonneg hj₁.le ( h_nonneg j hj₂ ) ;
    exact le_of_tendsto_of_tendsto tendsto_const_nhds h_cont ( by filter_upwards [ h_pos ] with j hj; exact hj );
  · -- Choose $c_n = n$ and $d_n = \frac{1}{n} d$.
    use fun n => n, fun n => (1 / n : ℝ) • d;
    -- Show that the sequence $y + \frac{1}{n} d$ converges to $y$ and is eventually in $U$.
    have h_seq_conv : Filter.Tendsto (fun n : ℕ => y + (1 / (n : ℝ)) • d) Filter.atTop (nhds y) := by
      simpa using tendsto_const_nhds.add ( tendsto_inverse_atTop_nhds_zero_nat.smul_const d );
    exact ⟨ Filter.eventually_atTop.mp ( h_seq_conv.eventually ( hU.mem_nhds hy_in_U ) ) |> fun ⟨ N, hN ⟩ => ⟨ N, fun n hn => ⟨ hN n hn, by simpa [ inner_add_left, inner_smul_left, hy_on_boundary ] using mul_nonneg ( inv_nonneg.2 ( Nat.cast_nonneg _ ) ) hd ⟩ ⟩, tendsto_natCast_atTop_atTop, tendsto_const_nhds.congr' <| by filter_upwards [ Filter.eventually_ne_atTop 0 ] with n hn; simp +decide [ hn ] ⟩

/-- The tangent cone to a closed half-space at a point on its boundary is the
    half-space itself (translated to the origin). -/
theorem posTangentConeAt_halfspace
    (n : E)
    (y : E) (hy_on_boundary : ⟪y, n⟫ = 0) :
    let H := {z | ⟪z, n⟫ ≥ 0}
    posTangentConeAt H y = {d | ⟪d, n⟫ ≥ 0} := by
  let H_origin := {d | ⟪d, n⟫ ≥ 0}
  ext d
  constructor
  -- Part 1: (⊆) the tangent cone is a subset of the half-space.
  · intro hd_in_cone
    obtain ⟨c, y', hy', hc, hcd⟩ := hd_in_cone
    have hy'_in_H : ∀ᶠ k in atTop, y + y' k ∈ H_origin := hy'
    have h_inner_seq : ∀ᶠ k in atTop, ⟪y + y' k, n⟫ ≥ 0 := hy'_in_H
    have h_inner_y' : ∀ᶠ k in atTop, ⟪y' k, n⟫ ≥ 0 := by
      filter_upwards [h_inner_seq] with k hk
      rwa [inner_add_left, hy_on_boundary, zero_add] at hk
    -- From Tendsto c atTop atTop, we get eventually 0 < c k.
    have hc_pos : ∀ᶠ k in atTop, 0 < c k :=
      hc.eventually_gt_atTop 0
    have h_inner_smul : ∀ᶠ k in atTop, ⟪c k • y' k, n⟫ ≥ 0 := by
      filter_upwards [h_inner_y', hc_pos] with k h_inner h_c
      rw [inner_smul_left]
      exact mul_nonneg (le_of_lt h_c) h_inner
    -- Limit of ⟪c k • y' k, n⟫ is ⟪d, n⟫.
    have h_inner_lim : Tendsto (fun k => ⟪c k • y' k, n⟫) atTop (𝓝 ⟪d, n⟫) :=
      Filter.Tendsto.inner hcd tendsto_const_nhds
    -- Since eventually 0 ≤ ⟪c k • y' k, n⟫, pass to the limit to get 0 ≤ ⟪d, n⟫.
    have : 0 ≤ ⟪d, n⟫ :=
      le_of_tendsto_of_tendsto tendsto_const_nhds h_inner_lim h_inner_smul
    exact this
  -- Part 2: (⊇) the half-space is a subset of the tangent cone.
  · intro hd_in_halfspace
    use fun k => (k + 1 : ℝ)
    use fun k => (1 / (k + 1 : ℝ)) • d
    refine ⟨?_, ?_, ?_⟩
    -- `y + y' k` is eventually in the set `H`.
    · apply Eventually.of_forall
      intro k
      show ⟪y + (1 / (k + 1 : ℝ)) • d, n⟫ ≥ 0
      rw [inner_add_left, hy_on_boundary, zero_add, inner_smul_left]
      have h_pos : 0 ≤ (1 / (k + 1 : ℝ)) := by positivity
      exact mul_nonneg h_pos hd_in_halfspace
    -- the sequence of scalars `c k` tends to `+∞`.
    · have : Tendsto (fun n : ℕ => (n : ℝ) + 1) atTop atTop := by
        apply Tendsto.atTop_add
        · exact tendsto_natCast_atTop_atTop
        · exact tendsto_const_nhds
      exact this
    -- the sequence `c k • y' k` converges to `d`.
    · have hconst :
          (fun k : ℕ => ((k : ℝ) + 1) • ((1 / ((k : ℝ) + 1)) • d)) = (fun _ => d) := by
        funext k
        have hk_ne : ((k : ℝ) + 1) ≠ 0 := by
          have hk_pos : 0 < ((k : ℝ) + 1) :=
            add_pos_of_nonneg_of_pos (by exact_mod_cast (Nat.zero_le k)) zero_lt_one
          exact ne_of_gt hk_pos
        have hk_mul_one_div : ((k : ℝ) + 1) * (1 / ((k : ℝ) + 1)) = (1 : ℝ) := by
          simpa [one_div] using (by simp_all only [ge_iff_le, mem_setOf_eq, ne_eq, not_false_eq_true, mul_inv_cancel₀])
        simp [smul_smul]; simp_all only [ge_iff_le, mem_setOf_eq, ne_eq, one_div, not_false_eq_true,
          mul_inv_cancel₀, one_smul]
      have : Tendsto (fun _ : ℕ => d) atTop (𝓝 d) := tendsto_const_nhds
      simp_all only [ge_iff_le, mem_setOf_eq, one_div, tendsto_const_nhds_iff]

/-- Intersecting with a neighborhood of `x` does not change the positive tangent cone. -/
lemma posTangentConeAt_inter_nhds
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (s t : Set E) (x : E) (ht : t ∈ 𝓝 x) :
    posTangentConeAt (s ∩ t) x = posTangentConeAt s x := by
  apply le_antisymm
  · exact (posTangentConeAt_mono (a := x) (by intro z hz; exact hz.1))
  · intro y hy
    rcases hy with ⟨c, d, hd, hc, hcd⟩
    have hc' : Tendsto (fun n => ‖c n‖) atTop atTop :=
      tendsto_abs_atTop_atTop.comp hc
    have hd0 : Tendsto d atTop (𝓝 (0 : E)) :=
      tangentConeAt.lim_zero (l := atTop) hc' hcd
    have hx_add : Tendsto (fun n => x + d n) atTop (𝓝 x) := by
      simpa [add_zero] using tendsto_const_nhds.add hd0
    have h_in_t : ∀ᶠ n in atTop, x + d n ∈ t := hx_add.eventually ht
    refine ⟨c, d, (hd.and h_in_t).mono (by intro n h; exact ⟨h.1, h.2⟩), hc, hcd⟩

/--
If a set `s` is the intersection of an open set `U` and a closed half-space `H`,
then the tangent cone to `s` at a point `y` that lies in `U` and on the boundary
of `H` is the half-space `H` translated to the origin.
-/
theorem posTangentConeAt_of_intersection_open_with_halfspace
    (U : Set E) (hU : IsOpen U)
    (n : E)
    (y : E) (hy_on_boundary : ⟪y, n⟫ = 0)
    (hy_in_U : y ∈ U) :
    posTangentConeAt (U ∩ {z | ⟪z, n⟫ ≥ 0}) y = {d | ⟪d, n⟫ ≥ 0} := by
  have hremove :
      posTangentConeAt (U ∩ {z | ⟪z, n⟫ ≥ 0}) y =
        posTangentConeAt ({z | ⟪z, n⟫ ≥ 0}) y := by
    simpa [inter_comm] using
      posTangentConeAt_inter_nhds
        (s := {z | ⟪z, n⟫ ≥ 0}) (t := U) (x := y) (hU.mem_nhds hy_in_U)
  simpa [hremove] using posTangentConeAt_halfspace (n := n) (y := y) hy_on_boundary

[Yury G. Kudryashov]

BTW, you can generalize it from inner product to any continuous linear map f : E -> Real (and from an inner product space to a normed space).