test module

`Tests.PairingRockafellarPotential`

0 named declarations scanned from Tests/PairingRockafellarPotential.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/PairingRockafellarPotential.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential

#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.rockafellarValueSet
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarPotential
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.rockafellarValueSet_nonempty
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.isGreatest_zero_properRockafellarValueSet_at_root
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarPotential_at_root_eq_zero
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.root_mem_effectiveDomain
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.effectiveDomain_nonempty
#check AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotential.properRockafellarPotential_at_root_eq_zero_of_distinct