production module

`AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient`

3 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexSubgradient.lean.

Imports

Mathlib.Analysis.Calculus.LocalExtr.Basic externalMathlib.Analysis.InnerProductSpace.Dual external

Imported by

AutoSamplingTheory.TechnicalLemmas.AnalysisAutoSamplingTheory.TechnicalLemmas.Analysis.ConvexLocalSubgradientTests.ConvexSubgradient

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient.SupportsAt Partial Not mapped

- `y` is a global Hilbert-space subgradient/supporting vector of `phi` at `x`. This is deliberately a pointwise relation; an OT coupling can later be required to be concentrated on this graph without first choosing a transport map.

def SupportsAt (phi : E → ℝ) (x y : E) : Prop :=
  ∀ z, phi x + (innerSL ℝ y) (z - x) ≤ phi z

/-- At a Frechet differentiability point, a supporting vector is the unique
Riesz representative of the derivative. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexSubgradient.lean:39published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient.eq_gradient_of_supportsAt_of_hasFDerivAt Partial Not mapped

- At a Frechet differentiability point, a supporting vector is the unique Riesz representative of the derivative.

theorem eq_gradient_of_supportsAt_of_hasFDerivAt
    {phi : E → ℝ} {x y g : E}
    (hsupport : SupportsAt phi x y)
    (hderiv : HasFDerivAt phi (innerSL ℝ g) x) :
    y = g := by
  have hmin : IsLocalMin (phi - fun z => (innerSL ℝ y) z) x := by
    filter_upwards with z
    have hz := hsupport z
    rw [map_sub] at hz
    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 hz _
  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

/-- In particular, two supporting vectors at the same differentiability point
coincide. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexSubgradient.lean:44published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradient.supportsAt_unique_of_hasFDerivAt Partial Not mapped

- In particular, two supporting vectors at the same differentiability point coincide.

theorem supportsAt_unique_of_hasFDerivAt
    {phi : E → ℝ} {x y₁ y₂ g : E}
    (h₁ : SupportsAt phi x y₁)
    (h₂ : SupportsAt phi x y₂)
    (hderiv : HasFDerivAt phi (innerSL ℝ g) x) :
    y₁ = y₂ := by
  rw [eq_gradient_of_supportsAt_of_hasFDerivAt h₁ hderiv,
    eq_gradient_of_supportsAt_of_hasFDerivAt h₂ hderiv]

end

end ConvexSubgradient
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexSubgradient.lean:65published source at 0e31a3cda412