English
The cardinality of the increment partition equals the step bound of the original partition's size, under certain assumptions.
Русский
Кардинал части приращения равен пределу шага для исходного разбиения при выполнении условий.
LaTeX
$$$\\lvert (increment hP G ε).parts \\rvert = \\mathrm{stepBound}(\\#P.parts)$$$
Lean4
/-- The increment partition has energy greater than the original one by a known fixed amount. -/
theorem energy_increment (hP : P.IsEquipartition) (hP₇ : 7 ≤ #P.parts) (hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5)
(hPα : #P.parts * 16 ^ #P.parts ≤ card α) (hPG : ¬P.IsUniform G ε) (hε₀ : 0 ≤ ε) (hε₁ : ε ≤ 1) :
↑(P.energy G) + ε ^ 5 / 4 ≤ (increment hP G ε).energy G :=
by
calc
_ = (∑ x ∈ P.parts.offDiag, (G.edgeDensity x.1 x.2 : ℝ) ^ 2 + #P.parts ^ 2 * (ε ^ 5 / 4) : ℝ) / #P.parts ^ 2 := by
rw [coe_energy, add_div, mul_div_cancel_left₀]; positivity
_ ≤
(∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, G.edgeDensity i.1 i.2 ^ 2 : ℝ) / 16 ^ #P.parts) /
#P.parts ^ 2 :=
?_
_ =
(∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, G.edgeDensity i.1 i.2 ^ 2 : ℝ) /
#(increment hP G ε).parts ^ 2 :=
by rw [card_increment hPα hPG, coe_stepBound, mul_pow, pow_right_comm, div_mul_eq_div_div_swap, ← sum_div];
norm_num
_ ≤ _ := by
rw [coe_energy]
gcongr
rw [← sum_biUnion pairwiseDisjoint_distinctPairs]
exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _
gcongr
rw [Finpartition.IsUniform, not_le, mul_tsub, mul_one, ← offDiag_card] at hPG
calc
_ ≤
∑ x ∈ P.parts.offDiag, (edgeDensity G x.1 x.2 : ℝ) ^ 2 +
(#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) :=
add_le_add_left ?_ _
_ =
∑ x ∈ P.parts.offDiag,
((G.edgeDensity x.1 x.2 : ℝ) ^ 2 + ((if G.IsUniform ε x.1 x.2 then (0 : ℝ) else ε ^ 4 / 3) - ε ^ 5 / 25) :
ℝ) :=
by
rw [sum_add_distrib, sum_sub_distrib, sum_const, nsmul_eq_mul, sum_ite, sum_const_zero, zero_add, sum_const,
nsmul_eq_mul, ← Finpartition.nonUniforms, ← add_sub_assoc, add_sub_right_comm]
_ = _ := (sum_attach ..).symm
_ ≤ _ := sum_le_sum fun i _ ↦ le_sum_distinctPairs_edgeDensity_sq i hε₁ hPα hPε
calc
_ = (6 / 7 * #P.parts ^ 2) * ε ^ 5 * (7 / 24) := by ring
_ ≤ #P.parts.offDiag * ε ^ 5 * (22 / 75) := by
gcongr ?_ * _ * ?_
· rw [← mul_div_right_comm, div_le_iff₀ (by simp), offDiag_card]
norm_cast
rw [tsub_mul]
refine le_tsub_of_add_le_left ?_
nlinarith
· norm_num
_ = (#P.parts.offDiag * ε * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by ring
_ ≤ (#(nonUniforms P G ε) * (ε ^ 4 / 3) - #P.parts.offDiag * (ε ^ 5 / 25)) := by gcongr
