O(μn)O(\mu{}n) expected optimization time for jump sizes k≤cln⁡ln⁡nk \le c \operatorname{ln} \operatorname{ln} n

Lax343628.LogLogJumpSizes · concepts/Lax343628/LogLogJumpSizes.lean · lax-343628

proven

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let TT be the optimization time of the (μ+1)(\mu+1) genetic algorithm with crossover probability pcp_c on Jumpk\mathrm{Jump}_k, started from μ\mu individuals chosen independently and uniformly at random from {0,1}n\{0,1\}^n.

    Let pc∈(0,1]p_c\in(0,1] and a>0a>0 be constants. If 1≤k≤cln⁡ln⁡n1\le k\le c\ln\ln n for a sufficiently small constant c>0c>0, and Ck(ln⁡n)2≤μ≤naCk(\ln n)^2\le\mu\le n^{a} for a sufficiently large constant CC, then E[T]=O(μn)\mathbb E[T]=O(\mu n).

    The constants cc, CC and the constant in O(μn)O(\mu n) depend only on pcp_c and aa. The bound holds for all sufficiently large nn, uniformly in kk and μ\mu.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax343628.Runtime
    2import Mathlib.Analysis.SpecialFunctions.Log.Basic
    3import Mathlib.Analysis.SpecialFunctions.Pow.Real
    4
    5/-!
    6---
    7title: O(μn)O(\mu{}n) expected optimization time for jump sizes k≤cln⁡ln⁡nk \le c \operatorname{ln} \operatorname{ln} n
    8type: theorem
    9---
    10Let TT be the optimization time of the (μ+1)(\mu+1) genetic algorithm with crossover probability
    11pcp_c on Jumpk\mathrm{Jump}_k, started from μ\mu individuals chosen independently and uniformly
    12at random from {0,1}n\{0,1\}^n.
    13
    14Let pc∈(0,1]p_c\in(0,1] and a>0a>0 be constants. If 1≤k≤cln⁡ln⁡n1\le k\le c\ln\ln n for a sufficiently small
    15constant c>0c>0, and Ck(ln⁡n)2≤μ≤naCk(\ln n)^2\le\mu\le n^{a} for a sufficiently large constant CC, then
    16E[T]=O(μn)\mathbb E[T]=O(\mu n).
    17
    18The constants cc, CC and the constant in O(μn)O(\mu n) depend only on pcp_c and aa.
    19The bound holds for all sufficiently large nn, uniformly in kk and μ\mu.
    20-/
    21
    22namespace Lax343628.LogLogJumpSizes
    23
    24open Lax343628.Algorithm Lax343628.Runtime Filter
    25open scoped ENNReal
    26
    27/-- E[T]≤Bμn\mathbb E[T]\le B\mu n for jump sizes 1≤k≤cln⁡ln⁡n1\le k\le c\ln\ln n and population sizes
    28Ck(ln⁡n)2≤μ≤naCk(\ln n)^2\le\mu\le n^a. Here BB is the constant in O(μn)O(\mu n). `∀ᶠ n in atTop` means
    29"for all sufficiently large nn"; since kk and μ\mu are quantified inside it, the threshold
    30for nn does not depend on them. -/
    31axiom 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
    42end Lax343628.LogLogJumpSizes
    43
    Show Proof

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…