production module

`AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarSupportGradient`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarSupportGradient.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexLocalSubgradientAutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarRealSupportMathlib.Analysis.Calculus.Gradient.Basic external

Imported by

AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalBrenierMapTests.PairingRockafellarSupportGradient

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem

AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarSupportGradient.eq_gradient_of_properSupportsAt_of_mem_interior

Partial Not mapped

- At an interior differentiability point of an extended-real potential's finite domain, every honest extended-real supporting vector is the gradient of the finite real representative.

theorem eq_gradient_of_properSupportsAt_of_mem_interior
    {Phi : E → WithTop ℝ} {x y : E}
    (hsupport : ProperSupportsAt Phi x y)
    (hx : x ∈ interior (EffectiveDomain Phi))
    (hdiff : DifferentiableAt ℝ (finitePart Phi) x) :
    y = gradient (finitePart Phi) x := by
  have hsupportOn :
      SupportsOn (EffectiveDomain Phi) (finitePart Phi) x y := by
    intro z hz
    exact finitePart_support_on_effectiveDomain hsupport z hz
  exact eq_gradient_of_supportsOn_of_hasFDerivAt
    hsupportOn
    (mem_interior_iff_mem_nhds.mp hx)
    hdiff.hasGradientAt.hasFDerivAt

/-- Relation-point specialization for the proper list-based Rockafellar
potential.  Closed-chain monotonicity supplies the support relation; interior
membership and differentiability perform the final analytic collapse. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarSupportGradient.lean:37published source at 0e31a3cda412

theorem AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarSupportGradient.snd_eq_gradient_of_mem_of_mem_interior Partial Not mapped

- Relation-point specialization for the proper list-based Rockafellar potential. Closed-chain monotonicity supplies the support relation; interior membership and differentiability perform the final analytic collapse.

theorem snd_eq_gradient_of_mem_of_mem_interior
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChain.PairingClosedChainMonotone Gamma)
    {x y : E} (hxy : (x, y) ∈ Gamma)
    (hx : x ∈ interior
      (EffectiveDomain (properRockafellarPotential base Gamma)))
    (hdiff : DifferentiableAt ℝ
      (finitePart (properRockafellarPotential base Gamma)) x) :
    y = gradient (finitePart (properRockafellarPotential base Gamma)) x := by
  exact eq_gradient_of_properSupportsAt_of_mem_interior
    (properSupportsAt_of_mem hbase hclosed hxy) hx hdiff

end

end PairingRockafellarSupportGradient
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarSupportGradient.lean:55published source at 0e31a3cda412