Source indexedlemma · leanprover/lean4:v4.32.0

smul_le_indicator

Carleson.ForestOperator.QuantativeEstimate · Carleson/ForestOperator/QuantativeEstimate.lean:522 to 533

Mathematical statement

Exact Lean statement

lemma smul_le_indicator {A : Set X} (hf : f.support ⊆ A) {C : ℝ} (hC : ∀ x, ‖f x‖ ≤ C)
    (hCpos : 0 < C) : ∀ x, ‖(C⁻¹ • f) x‖ ≤ A.indicator 1 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma smul_le_indicator {A : Set X} (hf : f.support ⊆ A) {C : ℝ} (hC : ∀ x, ‖f x‖ ≤ C)    (hCpos : 0 < C) : ∀ x, ‖(C⁻¹ • f) x‖ ≤ A.indicator 1 x := by  intro x  simp only [Pi.smul_apply, real_smul, ofReal_inv, Complex.norm_mul, norm_inv, norm_real,    Real.norm_eq_abs]  rw [inv_mul_le_iff₀ (by positivity),mul_comm,← indicator_mul_const]  simp only [Pi.one_apply, one_mul]  by_cases h : x ∈ A  · rw [indicator_of_mem h]    exact le_trans (hC x) (by exact le_abs_self C)  · rw [notMem_support.mp (fun a ↦ h (hf a)), indicator_of_notMem h]    simp only [norm_zero, le_refl]