Source indexedlemma · leanprover/lean4:v4.32.0

slice_integral_bound_sum

Carleson.MetricCarleson.Truncation · Carleson/MetricCarleson/Truncation.lean:172 to 188

Source documentation

The slightly unusual way of writing the integrand is to facilitate applying the monotone convergence theorem.

Exact Lean statement

lemma slice_integral_bound_sum :
    ∫⁻ x, (G \ (slice CP bG mG (n + 1)).G).indicator (‖T_lin CP.Q σ₁ σ₂ f ·‖ₑ) x ≤
    C2_0_1 a q * (∑ i ∈ Finset.range (n + 1), (2⁻¹ ^ i) ^ (q' : ℝ)⁻¹) *
    volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma slice_integral_bound_sum :    ∫⁻ x, (G \ (slice CP bG mG (n + 1)).G).indicator (‖T_lin CP.Q σ₁ σ₂ f ·‖ₑ) x ≤    C2_0_1 a q * (∑ i ∈ Finset.range (n + 1), (2⁻¹ ^ i) ^ (q' : ℝ)⁻¹) *    volume G ^ (q' : ℝ)⁻¹ * volume F ^ (q : ℝ)⁻¹ := by  rw [lintegral_indicator (mG.diff (slice CP bG mG _).mG)]  induction n with  | zero =>    rw [zero_add, Finset.range_one, Finset.sum_singleton, pow_zero, one_rpow, mul_one]    convert! slice_integral_bound; simp [slice]  | succ n ih =>    rw [← sdiff_union_sdiff_cancel _ slice_G_subset]; swap    · exact antitone_slice_G zero_le    rw [lintegral_union ((slice CP bG mG _).mG.diff (slice CP bG mG _).mG)]; swap    · exact disjoint_of_subset_right sdiff_subset disjoint_sdiff_left    rw [Finset.sum_range_succ, mul_add, add_mul, add_mul]; gcongr    rw [mul_assoc _ _ (volume G ^ _), ← ENNReal.mul_rpow_of_nonneg _ _ (by positivity)]    apply slice_integral_bound.trans; gcongr; exact volume_slice_le_inv_two_pow_mul