AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexLocalSubgradient

- `y` supports `phi` at `x` relative to a set `s`. Downstream proper-potential arguments will use `s` equal to the finite effective domain.

def SupportsOn (s : Set E) (phi : E → ℝ) (x y : E) : Prop :=
  ∀ z, z ∈ s → phi x + (innerSL ℝ y) (z - x) ≤ phi z

/-- A global support inequality restricts to any set. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexLocalSubgradient.lean:31published source at 0e31a3cda412

- A global support inequality restricts to any set.

theorem supportsOn_of_supportsAt
    {s : Set E} {phi : E → ℝ} {x y : E}
    (h : SupportsAt phi x y) :
    SupportsOn s phi x y := by
  intro z _hz
  exact h z

/-- If the relative support set is a neighborhood of `x`, then at a Frechet
point the supporting vector is exactly the Riesz representative of the
derivative. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexLocalSubgradient.lean:35published source at 0e31a3cda412

- If the relative support set is a neighborhood of `x`, then at a Frechet point the supporting vector is exactly the Riesz representative of the derivative.

theorem eq_gradient_of_supportsOn_of_hasFDerivAt
    {s : Set E} {phi : E → ℝ} {x y g : E}
    (hsupport : SupportsOn s phi x y)
    (hs : s ∈ 𝓝 x)
    (hderiv : HasFDerivAt phi (innerSL ℝ g) x) :
    y = g := by
  have hmin : IsLocalMin (phi - fun z => (innerSL ℝ y) z) x := by
    filter_upwards [hs] with z hz
    have h := hsupport z hz
    rw [map_sub] at h
    change phi x - (innerSL ℝ y) x ≤ phi z - (innerSL ℝ y) z
    calc
      phi x - (innerSL ℝ y) x =
          (phi x + ((innerSL ℝ y) z - (innerSL ℝ y) x)) - (innerSL ℝ y) z := by ring
      _ ≤ phi z - (innerSL ℝ y) z := sub_le_sub_right h _
  have hpsi := hderiv.sub (innerSL ℝ y).hasFDerivAt
  have hzero := hmin.hasFDerivAt_eq_zero hpsi
  have heq : innerSL ℝ g = innerSL ℝ y := sub_eq_zero.mp hzero
  exact (innerSL_inj.mp heq).symm

/-- Consequently, two vectors supporting the same real function on a
neighborhood of a differentiability point coincide. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexLocalSubgradient.lean:45published source at 0e31a3cda412

- Consequently, two vectors supporting the same real function on a neighborhood of a differentiability point coincide.

theorem supportsOn_unique_of_hasFDerivAt
    {s : Set E} {phi : E → ℝ} {x y₁ y₂ g : E}
    (h₁ : SupportsOn s phi x y₁)
    (h₂ : SupportsOn s phi x y₂)
    (hs : s ∈ 𝓝 x)
    (hderiv : HasFDerivAt phi (innerSL ℝ g) x) :
    y₁ = y₂ := by
  rw [eq_gradient_of_supportsOn_of_hasFDerivAt h₁ hs hderiv,
    eq_gradient_of_supportsOn_of_hasFDerivAt h₂ hs hderiv]

end

end ConvexLocalSubgradient
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexLocalSubgradient.lean:67published source at 0e31a3cda412