Expected optimization time

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

definition

Loading review…

Natural Language Statement

Definition

The $(\mu+1)$ genetic algorithm with crossover probability $p_c$ is run on $\mathrm{Jump}_k$ , starting from $\mu$ individuals chosen independently and uniformly at random from $\{0,1\}^n$ . Its optimization time $T$ is the number of iterations until the population first contains the optimum $1^n$ . The expected optimization time is $\mathbb E[T]$ .

Concept map

2 concepts; 2 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Lax343628.Algorithm
2	import Mathlib.Topology.Algebra.InfiniteSum.ENNReal
3
4	/-!
5	---
6	title: Expected optimization time
7	type: definition
8	---
9	The $(\mu+1)$ genetic algorithm with crossover probability $p_c$ is run on
10	$\mathrm{Jump}_k$ , starting from $\mu$ individuals chosen independently and uniformly at
11	random from $\{0,1\}^n$ . Its optimization time $T$ is the number of iterations until the
12	population first contains the optimum $1^n$ . The expected optimization time is $\mathbb E[T]$ .
13	-/
14
15	namespace Lax343628.Runtime
16
17	open Lax343628.Algorithm
18	open scoped ENNReal Classical BigOperators
19
20	noncomputable section
21
22	/-- The population distribution after $t$ iterations of the $(\mu+1)$ GA.
23	Initialization is uniform over all indexed populations, equivalently independent uniform
24	initial individuals. Each subsequent iteration uses `step` with fitness $\mathrm{Jump}_k$ . -/
25	def populationLaw (n k : ℕ) (μ : ℕ+) (p_c : ℝ) : ℕ → PMF (Population n μ)
26	\| 0 => PMF.uniformOfFintype (Population n μ)
27	\| t + 1 => do
28	let P ← populationLaw n k μ p_c t
29	step (jump k) p_c P
30
31	/-- The probability that the population after $t$ iterations does not contain $1^n$ .
32	For $1\le k\le n$ , this equals $\Pr[T>t]$ : since $1^n$ has the unique
33	maximal fitness, it is deleted only when all $\mu+1$ entries equal $1^n$ , so it is never
34	lost once present. -/
35	def tailProbability (n k : ℕ) (μ : ℕ+) (p_c : ℝ) (t : ℕ) : ℝ≥0∞ :=
36	∑ P : Population n μ with (∀ i, P i ≠ optimum n),
37	populationLaw n k μ p_c t P
38
39	/-- The expected optimization time $\mathbb E[T]=\sum_{t=0}^{\infty}\Pr[T>t]$ .
40	The sum is in nonnegative extended reals and may equal infinity. An optimum already present
41	in the initial population is found at time zero. -/
42	def expectedRuntime (n k : ℕ) (μ : ℕ+) (p_c : ℝ) : ℝ≥0∞ :=
43	∑' t : ℕ, tailProbability n k μ p_c t
44
45	end
46	end Lax343628.Runtime
47

Builds on

Lax343628.Algorithm

Used by

From Mathlib

Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Discussion

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

Loading discussion…

Lax Lean Archive

Expected optimization time

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments