Unbalancing

lemma unbalancing' (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (ν : G → ℝ≥0)    (f : G → ℝ) (g h : G → ℂ) (hf : g ○ᵈ g = (↑) ∘ f) (hν : h ○ᵈ h = (↑) ∘ ν)    (hν₁ : ∑ x, ν x = 1) (hε : ε ≤ ‖f‖_[p, ν]) :    ∃ p' : ℕ, p' ≤ 2 ^ 10 * ε⁻¹ ^ 2 * p ∧ 1 + ε / 2 ≤ ‖f + 1‖_[p', ν] := by  have := log_ε_pos hε₀ hε₁  have : 5 ≤ 2 * p + 3 := by omega  rw [← Nat.one_le_iff_ne_zero] at hp  refine ⟨⌈120 / ε * log (3 / ε) * p⌉₊, ?_, ?_⟩  · calc      (⌈120 / ε * log (3 / ε) * p⌉₊ : ℝ)        = ⌈120 * ε⁻¹ * log (3 * ε⁻¹) * p⌉₊ := by simp [div_eq_mul_inv]      _ ≤ 2 * (120 * ε⁻¹ * log (3 * ε⁻¹) * p) := Nat.ceil_le_two_mul <|        calc          (2⁻¹ : ℝ) ≤ 120 * 1 * 1 * 1 := by norm_num          _ ≤ 120 * ε⁻¹ * log (3 * ε⁻¹) * p := by            gcongr            · exact (one_le_inv₀ hε₀).2 hε₁            · rw [← log_exp 1]              gcongr              calc                exp 1 ≤ 2.7182818286 := exp_one_lt_d9.le                _ ≤ 3 * 1 := by norm_num                _ ≤ 3 * ε⁻¹ := by gcongr; exact (one_le_inv₀ hε₀).2 hε₁            · exact mod_cast hp      _ ≤ 2 * (120 * ε⁻¹ * (3 * ε⁻¹) * p) := by gcongr; exact Real.log_le_self (by positivity)      _ ≤ 2 * (2 ^ 7 * ε⁻¹ * (2 ^ 2 * ε⁻¹) * p) := by gcongr <;> norm_num      _ = 2 ^ 10 * ε⁻¹ ^ 2 * p := by ring  have hνprob : ∑ x, (ν x : ℝ≥0∞) = 1 := mod_cast hν₁  calc    1 + ε / 2 ≤ ↑‖f + 1‖_[.ofReal (24 / ε * log (3 / ε) * ↑(2 * p + 3)), ν] :=      unbalancing'' (2 * p + 3) this ((even_two_mul _).add_odd <| by decide) hε₀ hε₁ hf hν hν₁ <|        hε.trans <| wLpNorm_mono_right hνprob          (Nat.cast_le.2 <| le_add_of_le_left <| le_mul_of_one_le_left' one_le_two) _    _ ≤ _ := wLpNorm_mono_right hνprob ?_ _  norm_cast  calc    _ = 24 / ε * log (3 / ε) * ↑(2 * p + 3 * 1) := by simp    _ ≤ 24 / ε * log (3 / ε) * ↑(2 * p + 3 * p) := by gcongr    _ = 120 / ε * log (3 / ε) * p := by push_cast; ring    _ ≤ ⌈120 / ε * log (3 / ε) * p⌉₊ := Nat.le_ceil _