Source indexedlemma · leanprover/lean4:v4.32.0

MeasureTheory.distribution_pow

Carleson.ToMathlib.Distribution · Carleson/ToMathlib/Distribution.lean:212 to 218

Mathematical statement

Exact Lean statement

lemma distribution_pow (ε : Type*) [SeminormedRing ε] [NormOneClass ε] [NormMulClass ε] (f : α → ε)
    (t : ℝ≥0∞) (μ : Measure α) {n : ℕ} (hn : n ≠ 0) :
    distribution (f ^ n) (t ^ n) μ = distribution f t μ

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma distribution_pow (ε : Type*) [SeminormedRing ε] [NormOneClass ε] [NormMulClass ε] (f : α → ε)    (t : ℝ≥0∞) (μ : Measure α) {n : ℕ} (hn : n ≠ 0) :    distribution (f ^ n) (t ^ n) μ = distribution f t μ := by  simp_rw [distribution, Pi.pow_apply]  refine congrArg μ <| ext fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩  · rw [mem_setOf_eq, enorm_pow (f x) n] at hx; simpa using lt_of_pow_lt_pow_left' n hx  · rw [mem_setOf_eq, enorm_pow (f x) n]; exact ENNReal.pow_right_strictMono hn hx