General hoelder

lemma general_hoelder (hη : 0 ≤ η) (ν : G → ℝ≥0) (hfν : ∀ x, f x ≠ 0 → 1 ≤ ν x)    (hΔ : Δ ⊆ largeSpec f η) (hm : m ≠ 0) :    #Δ ^ (2 * m) * (η ^ (2 * m) * (‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2)) ≤      energy m Δ (dft fun a ↦ ν a) := by  obtain rfl | hf := eq_or_ne f 0  · simp  choose c norm_c hc using fun γ ↦ RCLike.exists_norm_eq_mul_self (dft f γ)  have :=    calc      η * ‖f‖_[1] * #Δ ≤ ∑ γ ∈ Δ, ‖dft f γ‖ := ?_      _ ≤ ‖∑ x, f x * ∑ γ ∈ Δ, c γ * conj (γ x)‖ := ?_      _ ≤ ∑ x, ‖f x * ∑ γ ∈ Δ, c γ * conj (γ x)‖ := (norm_sum_le _ _)      _ = ∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ := by simp_rw [norm_mul]      _ ≤ _ := inner_le_weight_mul_Lp_of_nonneg _ (p := m) ?_ _ _ (fun _ ↦ norm_nonneg _)            fun _ ↦ norm_nonneg _      _ = ‖f‖_[1] ^ (1 - (m : ℝ)⁻¹) * (∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ (m⁻¹ : ℝ) :=        by simp_rw [dL1Norm_eq_sum_norm, rpow_natCast]  rotate_left  · rw [← nsmul_eq_mul']    exact card_nsmul_le_sum _ _ _ fun x hx ↦ mem_largeSpec.1 <| hΔ hx  · simp_rw [mul_sum, mul_comm (f _), mul_assoc (c _), @sum_comm _ _ G, ← mul_sum, ← inner_apply',      ← wInner_one_eq_sum, ← dft_apply, ← hc, ← RCLike.ofReal_sum, RCLike.norm_ofReal]    exact le_abs_self _  · norm_cast    exact hm.bot_lt  replace this := pow_le_pow_left₀ (by positivity) this m  simp_rw [mul_pow] at this  rw [rpow_inv_natCast_pow _ hm, ← rpow_mul_natCast, one_sub_mul,    inv_mul_cancel₀, ← Nat.cast_pred, rpow_natCast, mul_assoc, mul_left_comm, ← pow_sub_one_mul,    mul_assoc, mul_le_mul_iff_right₀] at this  any_goals positivity  replace hfν : ∀ x, ‖f x‖ ≤ ‖f x‖ * sqrt (ν x) := by    rintro x    obtain hfx | hfx := eq_or_ne (f x) 0    · simp [hfx]    · exact le_mul_of_one_le_right (norm_nonneg _) <| one_le_sqrt.2 <| NNReal.one_le_coe.2 <|        hfν _ hfx  replace this :=    calc      (‖f‖_[1] * (η ^ m * #Δ ^ m)) ^ 2        ≤ (∑ x, ‖f x‖ * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by gcongr      _ ≤ (∑ x, ‖f x‖ * sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 := by        gcongr with x; exact hfν _      _ = (∑ x, ‖f x‖ * (sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m)) ^ 2 := by        simp_rw [mul_assoc]      _ ≤ (∑ x, ‖f x‖ ^ 2) * ∑ x, (sqrt (ν x) * ‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ m) ^ 2 :=        sum_mul_sq_le_sq_mul_sq _ _ _      _ ≤ ‖f‖_[2] ^ 2 * ∑ x, ν x * (‖∑ γ ∈ Δ, c γ * conj (γ x)‖ ^ 2) ^ m := by        simp_rw [dL2Norm_sq_eq_sum_norm, mul_pow, sq_sqrt (NNReal.coe_nonneg _), pow_right_comm]        rfl  rw [mul_rotate', mul_left_comm, mul_pow, mul_pow, ← pow_mul', ← pow_mul',    ← div_le_iff₀' (by positivity), mul_div_assoc, mul_div_assoc] at this  calc    _ ≤ _ := this    _ = ‖(_ : ℂ)‖ := Eq.symm <| RCLike.norm_of_nonneg <| sum_nonneg fun _ _ ↦ by positivity    _ = ‖∑ γ ∈ Δ ^^ m, ∑ δ ∈ Δ ^^ m,          (∏ i, conj (c (γ i)) * c (δ i)) * conj (dft (fun a ↦ ν a) (∑ i, γ i - ∑ i, δ i))‖ := ?_    _ ≤ ∑ γ ∈ Δ ^^ m, ∑ δ ∈ Δ ^^ m,          ‖(∏ i, conj (c (γ i)) * c (δ i)) * conj (dft (fun a ↦ ν a) (∑ i, γ i - ∑ i, δ i))‖ :=      (norm_sum_le _ _).trans <| sum_le_sum fun _ _ ↦ norm_sum_le _ _    _ = _ := by simp [energy, norm_c, norm_prod]  · push_cast    simp_rw [← RCLike.conj_mul, dft_apply, wInner_one_eq_sum, inner_apply', map_sum, map_mul,      RCLike.conj_conj, mul_pow, sum_pow', sum_mul, mul_sum, @sum_comm _ _ G,      ← AddChar.inv_apply_eq_conj, ← AddChar.neg_apply', prod_mul_prod_comm, ← AddChar.add_apply,      ← AddChar.sum_apply, mul_left_comm (Algebra.cast (ν _ : ℝ) : ℂ), ← mul_sum, ← sub_eq_add_neg,      sum_sub_distrib, Complex.conj_ofReal, mul_comm (Algebra.cast (ν _ : ℝ) : ℂ)]    rfl