Chang

lemma chang (hf : f ≠ 0) (hη : 0 < η) :    ∃ Δ, Δ ⊆ largeSpec f η ∧      #Δ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧      largeSpec f η ⊆ Δ.addSpan := by  refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_  obtain hΔ' | hΔ' := eq_zero_or_pos #Δ  · simp [hΔ']  let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G  have : 0 < α := by positivity  set β := ⌈𝓛 α⌉₊  have hβ : 0 < β := Nat.ceil_pos.2 (curlog_pos (by positivity) <| α_le_one _)  have : 0 < ‖f‖_[1] := by positivity  refine le_of_pow_le_pow_left₀ hβ.ne' zero_le <| Nat.cast_le.1 <| le_of_mul_le_mul_right ?_    (by positivity : 0 < #Δ ^ β * (η ^ (2 * β) * α))  push_cast  rw [← mul_assoc, ← pow_add, ← two_mul]  refine ((spec_hoelder hη.le hΔη hβ.ne').trans <| hΔ.boringEnergy_le _).trans ?_  refine le_trans ?_ <| mul_le_mul_of_nonneg_right (pow_le_pow_left₀ ?_ (Nat.le_ceil _) _) ?_  any_goals positivity  rw [mul_right_comm, div_pow, mul_pow, mul_pow, exp_one_pow, ← pow_mul, mul_div_assoc]  calc    _ = (changConst * #Δ * β) ^ β := by ring    _ ≤ (changConst * #Δ * β) ^ β * (α * exp β) := ?_    _ ≤ (changConst * #Δ * β) ^ β * ((η / η) ^ (2 * β) * α * exp β) := by      rw [div_self hη.ne', one_pow, one_mul]    _ = _ := by ring  refine le_mul_of_one_le_right (by positivity) ?_  rw [← inv_le_iff_one_le_mul₀' (by positivity)]  calc    α⁻¹ = exp (0 + log α⁻¹) := by rw [zero_add, exp_log]; positivity    _ ≤ exp ⌈0 + log α⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _    _ ≤ exp β := by unfold β; gcongr; exact zero_le_one