Scaling weights to integer multiplicities

Lax263307.WeightRounding · concepts/Lax263307/WeightRounding.lean · lax-263307

definition

Loading review…

Natural Language Statement

Definition

For nonnegative rational vertex weights, let $W$ be the maximum weight and choose $\tau=\varepsilon W/(2n)$ . The rounded multiplicity of vertex $v$ is $t_v=\lfloor w_v/\tau\rfloor$ . Vertices with $t_v=0$ are omitted from the independent blow-up.

Concept map

4 concepts; 5 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Lax263307.IndependentBlowUp
2	import Mathlib.Data.Finset.Max
3
4	/-!
5	---
6	title: Scaling weights to integer multiplicities
7	type: definition
8	---
9	For nonnegative rational vertex weights, let $W$ be the maximum weight and
10	choose $\tau=\varepsilon W/(2n)$ . The rounded multiplicity of vertex $v$ is
11	$t_v=\lfloor w_v/\tau\rfloor$ . Vertices with $t_v=0$ are omitted from the
12	independent blow-up.
13
14	# Formalization notes
15
16	The maximum includes zero, so it is defined also on the empty graph and on
17	signed weights before preprocessing. The rounding estimates assume
18	$n>0$ , $W>0$ , and $\varepsilon>0$ , ensuring $\tau>0$ .
19	The natural-valued floor is computed on exact rational numbers.
20	-/
21
22	namespace Lax263307.WeightRounding
23
24	/-- The maximum of the vertex weights and zero. -/
25	def maximumWeight {n : ℕ} (w : Fin n → ℚ) : ℚ :=
26	(insert 0 (Finset.univ.image w)).max' (by simp)
27
28	/-- The weight unit used by the reduction. -/
29	def scale {n : ℕ} (w : Fin n → ℚ) (ε : ℚ) : ℚ :=
30	ε * maximumWeight w / (2 * n)
31
32	/-- Multiplicities at a specified positive weight unit. -/
33	def roundedCopies {n : ℕ} (w : Fin n → ℚ) (τ : ℚ) : Fin n → ℕ :=
34	fun v => ⌊w v / τ⌋₊
35
36	/-- The multiplicities chosen for the requested accuracy. -/
37	def copies {n : ℕ} (w : Fin n → ℚ) (ε : ℚ) : Fin n → ℕ :=
38	roundedCopies w (scale w ε)
39
40	end Lax263307.WeightRounding
41

Formalization notes

The maximum includes zero, so it is defined also on the empty graph and on signed weights before preprocessing. The rounding estimates assume $n>0$ , $W>0$ , and $\varepsilon>0$ , ensuring $\tau>0$ . The natural-valued floor is computed on exact rational numbers.

Builds on

Lax263307.IndependentBlowUp

Used by

From Mathlib

Mathlib.Data.Finset.Max

Discussion

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

Loading discussion…

Lax Lean Archive

Scaling weights to integer multiplicities

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments