PL1/PartitionAverages.lean
All source files · Download exact source
SHA-256: 37e4a13e0a0694862b6e4b63fa9d9e2bf47f93d2168ddeeecc661635b20ed51c
1import PL1.TraceBounds23/-! # Contractive averages over finite measurable partitions -/45noncomputable section6set_option autoImplicit false7set_option maxHeartbeats 8000008open MeasureTheory9open scoped ENNReal BigOperators Topology1011namespace PL1.PartitionAverages1213variable {𝕜 Ω : Type*} [RCLike 𝕜] [MeasurableSpace Ω]14variable (μ : Measure Ω) [IsProbabilityMeasure μ]15variable (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i))1617def vector (i : ℕ) : Lp 𝕜 1 μ :=18 indicatorConstLp 1 (hA i) (measure_ne_top μ (A i)) (1 : 𝕜)1920theorem norm_vector (i : ℕ) : ‖vector (𝕜 := 𝕜) μ A hA i‖ = μ.real (A i) := by21 rw [vector, norm_indicatorConstLp (by norm_num) (by norm_num)]22 simp [measureReal_def]2324def coefficient (i : ℕ) : Lp 𝕜 1 μ →L[𝕜] 𝕜 :=25 (((μ.real (A i))⁻¹ : ℝ) : 𝕜) • TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i2627omit [IsProbabilityMeasure μ] in28theorem coefficient_apply (i : ℕ) (f : Lp 𝕜 1 μ) :29 coefficient (𝕜 := 𝕜) μ A hA i f = (((μ.real (A i))⁻¹ : ℝ) : 𝕜) * ∫ x in A i, f x ∂μ := by30 simp only [coefficient, smul_apply, TraceBounds.cellFunctional_apply, smul_eq_mul]3132def average (s : Finset ℕ) : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ :=33 ∑ i ∈ s, (coefficient (𝕜 := 𝕜) μ A hA i).smulRight (vector (𝕜 := 𝕜) μ A hA i)3435theorem average_apply (s : Finset ℕ) (f : Lp 𝕜 1 μ) :36 average μ A hA s f = ∑ i ∈ s, coefficient (𝕜 := 𝕜) μ A hA i f • vector (𝕜 := 𝕜) μ A hA i := by37 simp only [average, sum_apply, ContinuousLinearMap.smulRight_apply]3839theorem norm_coefficient_smul_vector_le (i : ℕ) (f : Lp 𝕜 1 μ) :40 ‖coefficient (𝕜 := 𝕜) μ A hA i f • vector (𝕜 := 𝕜) μ A hA i‖ ≤41 ‖TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i f‖ := by42 simp only [norm_smul, norm_vector, coefficient, smul_apply, norm_smul,43 RCLike.norm_ofReal, abs_inv, abs_of_nonneg (measureReal_nonneg)]44 by_cases hi : μ.real (A i) = 045 · simp [hi]46 · rw [mul_right_comm, inv_mul_cancel₀ hi, one_mul]4748theorem norm_average_apply_le (s : Finset ℕ)49 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) (f : Lp 𝕜 1 μ) :50 ‖average μ A hA s f‖ ≤ ‖f‖ := by51 rw [average_apply]52 calc53 _ ≤ ∑ i ∈ s, ‖coefficient (𝕜 := 𝕜) μ A hA i f • vector (𝕜 := 𝕜) μ A hA i‖ := norm_sum_le _ _54 _ ≤ ∑ i ∈ s, ‖TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i f‖ :=55 Finset.sum_le_sum (fun i _ => norm_coefficient_smul_vector_le μ A hA i f)56 _ ≤ ∑ i ∈ s, ‖L1Masks.mask μ (A i) (hA i) f‖ :=57 Finset.sum_le_sum (fun i _ => TraceBounds.norm_cellFunctional_apply_le_mask μ A hA i f)58 _ ≤ ‖f‖ := L1Masks.sum_norm_mask_le μ s A hA hdisj f5960theorem norm_average_le_one (s : Finset ℕ)61 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) :62 ‖average (𝕜 := 𝕜) μ A hA s‖ ≤ 1 := by63 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one64 intro f65 simpa only [one_mul] using norm_average_apply_le μ A hA s hdisj f6667theorem cellFunctional_vector68 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) (i j : ℕ) :69 TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i (vector (𝕜 := 𝕜) μ A hA j) =70 if i = j then (μ.real (A i) : 𝕜) else 0 := by71 rw [TraceBounds.cellFunctional_apply]72 unfold vector73 rw [integral_congr_ae (ae_restrict_of_ae74 (indicatorConstLp_coeFn (p := 1) (hs := hA j) (hμs := measure_ne_top μ (A j))75 (c := (1 : 𝕜)))), setIntegral_indicator (hA j)]76 by_cases hij : i = j77 · subst j78 simp [Algebra.smul_def]79 · rw [Set.disjoint_iff_inter_eq_empty.mp (hdisj hij)]80 simp [hij]8182theorem average_vector (s : Finset ℕ)83 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) (j : ℕ) (hj : j ∈ s) :84 average μ A hA s (vector (𝕜 := 𝕜) μ A hA j) = vector (𝕜 := 𝕜) μ A hA j := by85 by_cases hμ : μ.real (A j) = 086 · have hz : vector (𝕜 := 𝕜) μ A hA j = 0 := norm_eq_zero.mp (by rw [norm_vector, hμ])87 rw [hz, map_zero]88 · rw [average_apply]89 simp only [coefficient, smul_apply, cellFunctional_vector (𝕜 := 𝕜) μ A hA hdisj]90 rw [Finset.sum_eq_single j]91 · simp only [ite_true]92 rw [smul_eq_mul, ← RCLike.ofReal_mul, inv_mul_cancel₀ hμ, RCLike.ofReal_one, one_smul]93 · intro i hi hij94 simp [hij]95 · exact fun h => (h hj).elim9697theorem average_step (s : Finset ℕ)98 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) (c : ℕ → 𝕜) :99 average μ A hA s (∑ i ∈ s, c i • vector (𝕜 := 𝕜) μ A hA i) =100 ∑ i ∈ s, c i • vector (𝕜 := 𝕜) μ A hA i := by101 rw [map_sum]102 apply Finset.sum_congr rfl103 intro i hi104 rw [map_smul, average_vector (𝕜 := 𝕜) μ A hA s hdisj i hi]105106theorem norm_coefficient_le_of_ae_bound (i : ℕ) (f : Lp 𝕜 1 μ) (C : ℝ) (hC : 0 ≤ C)107 (hf : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : ‖coefficient (𝕜 := 𝕜) μ A hA i f‖ ≤ C := by108 have hi := norm_integral_le_of_norm_le_const (μ := μ.restrict (A i))109 (ae_restrict_of_ae hf)110 rw [coefficient_apply, norm_mul, RCLike.norm_ofReal,111 abs_inv, abs_of_nonneg (measureReal_nonneg)]112 by_cases hμ : μ.real (A i) = 0113 · simpa [hμ] using hC114 · calc115 _ ≤ (μ.real (A i))⁻¹ * (C * μ.real (A i)) :=116 mul_le_mul_of_nonneg_left (by simpa using hi) (inv_nonneg.mpr (measureReal_nonneg))117 _ = C := by field_simp118119theorem norm_coefficient_inclusion_le_one (i : ℕ) (f : Lp 𝕜 ∞ μ) (hf : ‖f‖ ≤ 1) :120 ‖coefficient (𝕜 := 𝕜) μ A hA i (ProbabilityLp.inclusion μ 1 ∞ le_top f)‖ ≤ 1 := by121 apply norm_coefficient_le_of_ae_bound μ A hA i _ 1 zero_le_one122 filter_upwards [ProbabilityLp.coeFn_inclusion μ 1 ∞ le_top f,123 ae_le_eLpNormEssSup (f := (f : Ω → 𝕜))] with x hx hnorm124 rw [hx]125 have h := ENNReal.toReal_mono (show eLpNormEssSup (f : Ω → 𝕜) μ ≠ ∞ from (Lp.memLp f).2.ne) hnorm126 have h' : ‖f x‖ ≤ ‖f‖ := by simpa only [toReal_enorm, Lp.norm_def, eLpNorm_exponent_top] using h127 exact h'.trans hf128129end PL1.PartitionAverages130131