AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarRealSupport

- An extended-real supporting vector becomes an ordinary supporting inequality for `finitePart` after restricting the comparison point to the finite effective domain.

theorem finitePart_support_on_effectiveDomain
    {Phi : E → WithTop ℝ} {x y : E}
    (hsupport : ProperSupportsAt Phi x y) :
    ∀ z, z ∈ EffectiveDomain Phi →
      finitePart Phi x + inner ℝ y (z - x) ≤ finitePart Phi z := by
  rcases hsupport with ⟨rx, hx, hsupport⟩
  intro z hz
  have hzlt : Phi z < ⊤ := hz
  have hcoe :
      (((rx + inner ℝ y (z - x) : ℝ) : ℝ) : WithTop ℝ) ≤
        ((finitePart Phi z : ℝ) : WithTop ℝ) := by
    rw [coe_finitePart_of_lt_top hzlt]
    exact hsupport z
  have hreal : rx + inner ℝ y (z - x) ≤ finitePart Phi z :=
    WithTop.coe_le_coe.mp hcoe
  have hxreal : finitePart Phi x = rx := by
    simp [finitePart, hx]
  rw [hxreal]
  exact hreal

/-- Specialized consumer-facing form for points of a closed-chain-monotone
relation. -/

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarRealSupport.lean:32published source at 0e31a3cda412

- Specialized consumer-facing form for points of a closed-chain-monotone relation.

theorem finitePart_support_on_effectiveDomain_of_mem
    {base : E × E} {Gamma : Set (E × E)}
    (hbase : base ∈ Gamma)
    (hclosed : PairingClosedChain.PairingClosedChainMonotone Gamma)
    {x y : E} (hxy : (x, y) ∈ Gamma) :
    ∀ z, z ∈ EffectiveDomain (properRockafellarPotential base Gamma) →
      finitePart (properRockafellarPotential base Gamma) x +
          inner ℝ y (z - x) ≤
        finitePart (properRockafellarPotential base Gamma) z :=
  finitePart_support_on_effectiveDomain
    (properSupportsAt_of_mem hbase hclosed hxy)

end

end PairingRockafellarRealSupport
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarRealSupport.lean:54published source at 0e31a3cda412