global_dichotomy

public lemma global_dichotomy [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpace G]    (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)    (hAC : ε ≤ |card G * ⟪μ_[ℝ] A ∗ᵈ μ A, μ C⟫_[ℝ] - 1|) :    ε / (2 * card G) ≤ ‖balance (μ_[ℝ] A) ○ᵈ balance (μ A)‖_[↑(2 * ⌈𝓛 γ⌉₊), μ univ] := by  have hC : C.Nonempty := by simpa using hγ.trans_le hγC  have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)  set p := 2 * ⌈𝓛 γ⌉₊  have hp : 1 < p :=    Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le <| Nat.ceil_pos.2 <| curlog_pos hγ.le hγ₁)  have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one_of_one_lt₀ <| mod_cast hp  have hp'' : (p : ℝ≥0).HolderConjugate _ := .conjExponent <| mod_cast hp  have : (p : ℝ≥0∞).HolderConjugate _ := hp''.coe_ennreal  rw [mul_comm, ← div_div, div_le_iff₀ (zero_lt_two' ℝ)]  calc    _ ≤ _ := div_le_div_of_nonneg_right hAC (card G).cast_nonneg    _ = |⟪balance (μ A) ∗ᵈ balance (μ A), μ C⟫_[ℝ]| := ?_    _ ≤ ‖balance (μ_[ℝ] A) ∗ᵈ balance (μ A)‖_[p] * ‖μ_[ℝ] C‖_[NNReal.conjExponent p] :=        abs_wInner_one_le_dLpNorm_mul_dLpNorm _ _    _ ≤ ‖balance (μ_[ℝ] A) ○ᵈ balance (μ A)‖_[p] * (card G ^ (-(p : ℝ)⁻¹) * γ ^ (-(p : ℝ)⁻¹)) :=        mul_le_mul (dLpNorm_ddconv_le_dLpNorm_dddconv' (by positivity) (even_two_mul _) _) ?_          (by positivity) (by positivity)    _ = ‖balance (μ_[ℝ] A) ○ᵈ balance (μ A)‖_[↑(2 * ⌈𝓛 γ⌉₊), μ univ] * γ ^ (-(p : ℝ)⁻¹) := ?_    _ ≤ _ := mul_le_mul_of_nonneg_left ?_ <| by positivity  · rw [← balance_ddconv, balance, wInner_sub_left, wInner_one_const_left, expect_ddconv,      sum_mu ℝ hA, expect_mu ℝ hA, sum_mu ℝ hC, conj_trivial, one_mul, one_mul, ← mul_inv_cancel₀,      ← mul_sub, abs_mul, abs_of_nonneg, mul_div_cancel_left₀] <;> positivity  · rw [dLpNorm_mu hp''.symm.lt.le hC, hp''.symm.coe.inv_sub_one, NNReal.coe_natCast, ← mul_rpow]    any_goals positivity    rw [nnratCast_dens, le_div_iff₀, mul_comm] at hγC    any_goals positivity    refine rpow_le_rpow_of_nonpos ?_ hγC (neg_nonpos.2 ?_) <;> positivity  · rw [mul_comm, mu_univ_eq_const, wLpNorm_const_right, mul_right_comm, rpow_neg, ← inv_rpow]    any_goals positivity    · congr    · exact ENNReal.natCast_ne_top _  · have : 1 ≤ γ⁻¹ := (one_le_inv₀ hγ).2 hγ₁    have : 0 ≤ log γ⁻¹ := by bound    calc      γ ^ (-(↑p)⁻¹ : ℝ) = √(γ⁻¹ ^ ((↑⌈1 + log γ⁻¹⌉₊)⁻¹ : ℝ)) := by        rw [rpow_neg hγ.le, inv_rpow hγ.le]        unfold p        push_cast        rw [mul_inv_rev, rpow_mul, sqrt_eq_rpow, one_div, inv_rpow] <;> positivity      _ ≤ √(γ⁻¹ ^ ((1 + log γ⁻¹)⁻¹ : ℝ)) := by grw [← Nat.le_ceil]      _ ≤ √ (exp 1) := by gcongr; exact rpow_inv_neg_curlog_le hγ.le hγ₁      _ ≤ √ 2.7182818286 := by gcongr; exact exp_one_lt_d9.le      _ ≤ 2 := by rw [sqrt_le_iff]; norm_num