expected optimization time for jump sizes
Lax343628.LogLogJumpSizes · concepts/Lax343628/LogLogJumpSizes.lean · lax-343628
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
Let be the optimization time of the genetic algorithm with crossover probability on , started from individuals chosen independently and uniformly at random from .
Let and be constants. If for a sufficiently small constant , and for a sufficiently large constant , then .
The constants , and the constant in depend only on and . The bound holds for all sufficiently large , uniformly in and .
Concept map
Lean source view on GitHub
| 1 | import Lax343628.Runtime |
| 2 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 3 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 4 | |
| 5 | /-! |
| 6 | --- |
| 7 | title: expected optimization time for jump sizes |
| 8 | type: theorem |
| 9 | --- |
| 10 | Let be the optimization time of the genetic algorithm with crossover probability |
| 11 | on , started from individuals chosen independently and uniformly |
| 12 | at random from . |
| 13 | |
| 14 | Let and be constants. If for a sufficiently small |
| 15 | constant , and for a sufficiently large constant , then |
| 16 | . |
| 17 | |
| 18 | The constants , and the constant in depend only on and . |
| 19 | The bound holds for all sufficiently large , uniformly in and . |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax343628.LogLogJumpSizes |
| 23 | |
| 24 | open Lax343628.Algorithm Lax343628.Runtime Filter |
| 25 | open scoped ENNReal |
| 26 | |
| 27 | /-- for jump sizes and population sizes |
| 28 | . Here is the constant in . `∀ᶠ n in atTop` means |
| 29 | "for all sufficiently large "; since and are quantified inside it, the threshold |
| 30 | for does not depend on them. -/ |
| 31 | axiom runtime_bound |
| 32 | (p_c a : ℝ) (hp_c : 0 < p_c ∧ p_c ≤ 1) (ha : 0 < a) : |
| 33 | ∃ c C B : ℝ, 0 < c ∧ 0 < C ∧ 0 < B ∧ |
| 34 | ∀ᶠ (n : ℕ) in atTop, |
| 35 | ∀ (k : ℕ) (μ : ℕ+), |
| 36 | 1 ≤ k → (k : ℝ) ≤ c * Real.log (Real.log (n : ℝ)) → |
| 37 | C * (k : ℝ) * (Real.log (n : ℝ)) ^ 2 ≤ (μ : ℕ) → |
| 38 | (μ : ℕ) ≤ (n : ℝ) ^ a → |
| 39 | expectedRuntime n k μ p_c ≤ |
| 40 | ENNReal.ofReal (B * (μ : ℕ) * (n : ℝ)) |
| 41 | |
| 42 | end Lax343628.LogLogJumpSizes |
| 43 |
Builds on
Used by
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments