3. Consistency equivalence🔗

We prove the equivalence between sample_whole_space and is_consistent for any stochastic iterative global optimization Algorithm A. This corresponds to Proposition 3 of the paper Cédric Malherbe and Nicolas Vayatis, 2017. “Global optimization of Lipschitz functions”. In International conference on machine learning..

theorem declaration uses `sorry`sample_iff_consistent (A : Algorithm α ℝ) :
    (∀ ⦃f : α → ℝ⦄, (hf : Lipschitz f) → sample_whole_space A hf.continuous)
    ↔
    (∀ ⦃f : α → ℝ⦄, (hf : Lipschitz f) → is_consistent A hf) := byα:Type u_1inst✝⁴:MeasurableSpace αinst✝³:PseudoMetricSpace αinst✝²:CompactSpace αinst✝¹:Nonempty αinst✝:OpensMeasurableSpace αA:Algorithm α ℝ⊢ (∀ ⦃f : α → ℝ⦄ (hf : Lipschitz f), sample_whole_space A ⋯) ↔ ∀ ⦃f : α → ℝ⦄ (hf : Lipschitz f), is_consistent A hf

The proof of the proposition is available in the ArXiv preprint of the original paper (Malherbe and Vayatis, 2017)Marginal noteCédric Malherbe and Nicolas Vayatis, 2017. “Global optimization of Lipschitz functions”. arXiv:1703.02628. We follow the same structure while adapting the proof to the Lean formalization. We also fixed a small mistake in the original proof, which was pointed out to the authors in a private discussion.

The modus ponens direction is easy to prove, as the continuity of f implies that sequences of samples such that, the maximum of their evaluations under f is at least \varepsilon, do not belong to a ball centered on the maximum of f with positive radius. The sample_whole_space hypothesis implies that the set of such sequences has measure tending to 0 as n tends to infinity, which proves is_consistent.

The converse direction is more involved. The proof is done by contradiction: if the algorithm does not sample the whole space for a given function f, then there exists a ball such that the measure of the set of sequences of samples that do not belong to this ball does not tend to 0 as n tends to infinity. The idea is to construct a function \tilde{f} that is indistinguishable from f outside of this ball, such that the maximum of \tilde{f} is strictly greater than the maximum of f and such that the \arg \max of \tilde{f} is inside the ball. This contradicts the is_consistent hypothesis, as the maximum of \tilde{f} is almost never sampled by the algorithm.

Our construction of the function \tilde{f} has a slightly simpler expression than the one in the original paper but provides the same properties. For more details, see Indistinguishable function.