diff --git a/BonnAnalysis/Dual.lean b/BonnAnalysis/Dual.lean index 8601113..8633c7b 100644 --- a/BonnAnalysis/Dual.lean +++ b/BonnAnalysis/Dual.lean @@ -48,8 +48,7 @@ lemma one_le_right (hpq : p.IsConjExponent q) : 1 ≤ q := hpq.symm.one_le_left lemma left_ne_zero (hpq : p.IsConjExponent q) : p ≠ 0 := zero_lt_one.trans_le hpq.one_le_left |>.ne' -lemma right_ne_zero (hpq : p.IsConjExponent q) : q ≠ 0 := - hpq.symm.left_ne_zero +lemma right_ne_zero (hpq : p.IsConjExponent q) : q ≠ 0 := hpq.symm.left_ne_zero lemma left_inv_ne_top (hpq : p.IsConjExponent q) : p⁻¹ ≠ ∞ := by rw [inv_ne_top] @@ -107,9 +106,9 @@ lemma toNNReal {p q : ℝ≥0∞} (hp : p ≠ ∞) (hq : q ≠ ∞) (hpq : p.IsC · exact (toNNReal_ne_zero).mpr ⟨hpq.left_ne_zero, hp⟩ lemma mul_eq_add (hpq : p.IsConjExponent q) : p * q = p + q := by - induction p using recTopCoe + induction p . simp [hpq.right_ne_zero] - induction q using recTopCoe + induction q . simp [hpq.left_ne_zero] norm_cast exact hpq.toNNReal coe_ne_top coe_ne_top |>.mul_eq_add @@ -119,9 +118,9 @@ lemma induction (nnreal : ∀ ⦃p q : ℝ≥0⦄, (h : p.IsConjExponent q) → P p q h.coe_ennreal) (one : P 1 ∞ one_top) (infty : P ∞ 1 top_one) {p q : ℝ≥0∞} (h : p.IsConjExponent q) : P p q h := by - induction p using recTopCoe + induction p . simp_rw [h.left_eq_top_iff.mp rfl, infty] - induction q using recTopCoe + induction q . simp_rw [h.left_eq_one_iff.mpr rfl, one] exact nnreal <| h.toNNReal coe_ne_top coe_ne_top @@ -153,14 +152,14 @@ lemma _root_.ENNReal.lintegral_mul_le_one_top (μ : Measure α) {f g : α → rw [Filter.eventually_iff, ← Filter.exists_mem_subset_iff] use {a | g a ≤ essSup g μ} rw [← Filter.eventually_iff] - exact ⟨ae_le_essSup _, by simp; intro _ ha; apply ENNReal.mul_left_mono ha⟩ + exact ⟨ae_le_essSup _, by simp; intro _ ha; exact ENNReal.mul_left_mono ha⟩ _ = (∫⁻ (a : α), f a ∂μ) * (essSup g μ) := by rw [lintegral_mul_const'' _ hf] lemma _root_.ENNReal.lintegral_norm_mul_le_one_top (μ : Measure α) {f : α → E₁} {g : α → E₂} (hf : AEMeasurable f μ) : ∫⁻ a, ‖f a‖₊ * ‖g a‖₊ ∂μ ≤ snorm f 1 μ * snorm g ⊤ μ := by simp [snorm, snorm', snormEssSup] - apply lintegral_mul_le_one_top _ hf.ennnorm + exact lintegral_mul_le_one_top _ hf.ennnorm theorem lintegral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : α → E₁} {g : α → E₂} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : @@ -192,9 +191,9 @@ theorem integrable_bilin (hpq : p.IsConjExponent q) (μ : Measure α) {f : α (hf : Memℒp f p μ) (hg : Memℒp g q μ) : Integrable (fun a ↦ L (f a) (g a)) μ := by use L.aestronglyMeasurable_comp₂ hf.aestronglyMeasurable hg.aestronglyMeasurable - apply lintegral_mul_le L hpq μ hf.aestronglyMeasurable.aemeasurable - hg.aestronglyMeasurable.aemeasurable |>.trans_lt - exact ENNReal.mul_lt_top (ENNReal.mul_ne_top coe_ne_top hf.snorm_ne_top) hg.snorm_ne_top + exact lintegral_mul_le L hpq μ hf.aestronglyMeasurable.aemeasurable + hg.aestronglyMeasurable.aemeasurable |>.trans_lt (ENNReal.mul_lt_top + (ENNReal.mul_ne_top coe_ne_top hf.snorm_ne_top) hg.snorm_ne_top) end IsConjExponent @@ -247,64 +246,53 @@ lemma p_ne_zero : p ≠ 0 := left_ne_zero hpq.out lemma p_ne_top : p ≠ ∞ := lt_top_iff_ne_top.mp h'p.out -lemma p_ne_zero' : p.toReal ≠ 0 := by - apply toReal_ne_zero.mpr - exact ⟨p_ne_zero (q := q), p_ne_top⟩ +lemma p_ne_zero' : p.toReal ≠ 0 := toReal_ne_zero.mpr ⟨p_ne_zero (q := q), p_ne_top⟩ lemma p_gt_zero : p > 0 := by - calc p ≥ 1 := by exact hp.out - _ > 0 := by simp + calc p ≥ 1 := hp.out + _ > 0 := zero_lt_one' ℝ≥0∞ -lemma p_gt_zero' : p.toReal > 0 := by - apply (toReal_pos_iff_ne_top p).mpr - exact p_ne_top +lemma p_gt_zero' : p.toReal > 0 := (toReal_pos_iff_ne_top p).mpr p_ne_top -lemma p_ge_zero : p ≥ 0 := by simp +lemma p_ge_zero : p ≥ 0 := zero_le p -lemma p_ge_zero' : p.toReal ≥ 0 := by apply toReal_nonneg +lemma p_ge_zero' : p.toReal ≥ 0 := toReal_nonneg lemma q_ne_zero : q ≠ 0 := right_ne_zero hpq.out -lemma q_ne_zero' (hqᵢ : q ≠ ∞) : q.toReal ≠ 0 := by - apply toReal_ne_zero.mpr - exact ⟨q_ne_zero (p := p), hqᵢ⟩ +lemma q_ne_zero' (hqᵢ : q ≠ ∞) : q.toReal ≠ 0 := toReal_ne_zero.mpr ⟨q_ne_zero (p := p), hqᵢ⟩ lemma q_gt_zero : q > 0 := by - calc q ≥ 1 := by exact hq.out - _ > 0 := by simp + calc q ≥ 1 := hq.out + _ > 0 := p_gt_zero -lemma q_gt_zero' (hqᵢ : q ≠ ∞) : q.toReal > 0 := by - apply (toReal_pos_iff_ne_top q).mpr - exact hqᵢ +lemma q_gt_zero' (hqᵢ : q ≠ ∞) : q.toReal > 0 := (toReal_pos_iff_ne_top q).mpr hqᵢ -lemma q_ge_zero : q ≥ 0 := by simp +lemma q_ge_zero : q ≥ 0 := p_ge_zero -lemma q_ge_zero' : q.toReal ≥ 0 := by aesop +lemma q_ge_zero' : q.toReal ≥ 0 := p_ge_zero' -lemma q_gt_one : q > 1 := by exact (left_ne_top_iff hpq.out).mp p_ne_top +lemma q_gt_one : q > 1 := (left_ne_top_iff hpq.out).mp p_ne_top lemma q_gt_one' (hqᵢ : q ≠ ∞) : q.toReal > 1 := by rw [←ENNReal.one_toReal] apply (ENNReal.toReal_lt_toReal _ _).mpr . show q > 1 apply q_gt_one (q := q) (p := p) - . simp + . exact Ne.symm top_ne_one . exact hqᵢ lemma q_ge_one : q ≥ 1 := by apply le_of_lt; exact q_gt_one (p := p) lemma q_ge_one' (hqᵢ : q ≠ ∞) : q.toReal ≥ 1 := by - rw [←ENNReal.one_toReal] + rw [← ENNReal.one_toReal] apply (ENNReal.toReal_le_toReal _ _).mpr - . show q ≥ 1 - apply q_ge_one (q := q) (p := p) - . simp + . exact q_ge_one (q := q) (p := p) + . exact Ne.symm top_ne_one . exact hqᵢ -lemma q_sub_one_pos' (hqᵢ : q ≠ ∞) : q.toReal - 1 > 0 := by - apply sub_pos.mpr - show q.toReal > 1 - exact q_gt_one' (q := q) (p := p) hqᵢ +lemma q_sub_one_pos' (hqᵢ : q ≠ ∞) : q.toReal - 1 > 0 := + sub_pos.mpr (q_gt_one' (q := q) (p := p) hqᵢ) lemma q_sub_one_nneg' (hqᵢ : q ≠ ∞) : q.toReal - 1 ≥ 0 := by linarith [q_sub_one_pos' (q := q) (p := p) hqᵢ] @@ -312,7 +300,7 @@ lemma q_sub_one_nneg' (hqᵢ : q ≠ ∞) : q.toReal - 1 ≥ 0 := by lemma p_add_q : p + q = p * q := hpq.out.mul_eq_add.symm lemma p_add_q' (hqᵢ : q ≠ ∞) : p.toReal + q.toReal = p.toReal*q.toReal := by - rw [←toReal_add p_ne_top hqᵢ, ←toReal_mul] + rw [← toReal_add p_ne_top hqᵢ, ← toReal_mul] congr exact p_add_q @@ -325,22 +313,22 @@ lemma q_div_p_ne_top (hqᵢ : q ≠ ∞) : q / p ≠ ∞ := by . intro _; contradiction lemma q_div_p_add_one : q / p + 1 = q := by - calc _ = q / p + p / p := by rw[ENNReal.div_self (p_ne_zero (q := q)) p_ne_top]; - _ = (q + p) / p := by rw[←ENNReal.add_div] - _ = (p + q) / p := by rw[add_comm] - _ = (p * q) / p := by rw[p_add_q] - _ = (p * q) / (p * 1) := by rw[mul_one] - _ = q / 1 := by rw[ENNReal.mul_div_mul_left _ _ (p_ne_zero (q := q)) p_ne_top] - _ = q := by rw[div_one] + calc _ = q / p + p / p := by rw [ENNReal.div_self (p_ne_zero (q := q)) p_ne_top]; + _ = (q + p) / p := by rw [← ENNReal.add_div] + _ = (p + q) / p := by rw [add_comm] + _ = (p * q) / p := by rw [p_add_q] + _ = (p * q) / (p * 1) := by rw [mul_one] + _ = q / 1 := by rw [ENNReal.mul_div_mul_left _ _ (p_ne_zero (q := q)) p_ne_top] + _ = q := div_one q lemma q_div_p_add_one' (hqᵢ : q ≠ ∞) : q.toReal / p.toReal + 1 = q.toReal := by - calc _ = (q / p).toReal + 1 := by rw[toReal_div] - _ = (q / p + 1).toReal := by rw[toReal_add]; simp; exact q_div_p_ne_top hqᵢ; simp - _ = q.toReal := by rw[q_div_p_add_one] + calc _ = (q / p).toReal + 1 := by rw [toReal_div] + _ = (q / p + 1).toReal := by rw [toReal_add]; simp; exact q_div_p_ne_top hqᵢ; simp + _ = q.toReal := by rw [q_div_p_add_one] lemma q_div_p_add_one'' (hqᵢ : q ≠ ∞) : q.toReal / p.toReal = q.toReal - 1 := by - calc _ = q.toReal / p.toReal + 1 - 1 := by simp - _ = q.toReal - 1 := by rw[q_div_p_add_one' hqᵢ] + calc _ = q.toReal / p.toReal + 1 - 1 := Eq.symm (add_sub_cancel_right (q.toReal / p.toReal) 1) + _ = q.toReal - 1 := by rw [q_div_p_add_one' hqᵢ] end BasicFactsConjugateExponents @@ -508,16 +496,14 @@ theorem integral_mul_le (hpq : p.IsConjExponent q) (μ : Measure α) {f : Lp E have : ∫⁻ (a : α), ↑‖(L (f a)) (g a)‖₊ ∂μ ≤ ↑‖L‖₊ * snorm (f) p μ * snorm (g) q μ := by apply lintegral_mul_le L hpq μ - . apply aestronglyMeasurable_iff_aemeasurable.mp - apply (Lp.memℒp f).aestronglyMeasurable - . apply aestronglyMeasurable_iff_aemeasurable.mp - apply (Lp.memℒp g).aestronglyMeasurable + . exact aestronglyMeasurable_iff_aemeasurable.mp (Lp.memℒp f).aestronglyMeasurable + . exact aestronglyMeasurable_iff_aemeasurable.mp (Lp.memℒp g).aestronglyMeasurable gcongr apply mul_ne_top; apply mul_ne_top - . simp [this] - . apply snorm_ne_top f - . apply snorm_ne_top g + . exact Ne.symm top_ne_coe + . exact snorm_ne_top f + . exact snorm_ne_top g section conj_q_lt_top' @@ -567,20 +553,15 @@ theorem conj_q_lt_top'_aemeasurable (g : Lp ℝ q μ) apply AEMeasurable.mul <;> apply Measurable.comp_aemeasurable' . exact measurable_sign . exact (Lp.memℒp g).aestronglyMeasurable.aemeasurable - . apply ENNReal.measurable_toReal - . apply Measurable.comp_aemeasurable' - . apply ENNReal.measurable_rpow'_const - . apply Measurable.comp_aemeasurable' - . apply measurable_coe_nnreal_ennreal - . apply Measurable.comp_aemeasurable' - . apply measurable_nnnorm - . exact (Lp.memℒp g).aestronglyMeasurable.aemeasurable + . exact ENNReal.measurable_toReal + . exact Measurable.comp_aemeasurable' (ENNReal.measurable_rpow'_const _) + (Measurable.comp_aemeasurable' (measurable_coe_nnreal_ennreal) (Measurable.comp_aemeasurable' + (measurable_nnnorm) (Lp.memℒp g).aestronglyMeasurable.aemeasurable)) @[measurability] theorem conj_q_lt_top'_aestrongly_measurable (g : Lp ℝ q μ) - : AEStronglyMeasurable (conj_q_lt_top' g) μ := by - apply (aestronglyMeasurable_iff_aemeasurable (μ := μ)).mpr - exact conj_q_lt_top'_aemeasurable g + : AEStronglyMeasurable (conj_q_lt_top' g) μ := (aestronglyMeasurable_iff_aemeasurable (μ := μ)).mpr + (conj_q_lt_top'_aemeasurable g) theorem conj_q_lt_top'_of_ae_eq_zero (g : Lp ℝ q μ) (hg : g =ᵐ[μ] 0) (hq₁ : q > 1) (hqᵢ : q ≠ ∞) : conj_q_lt_top' g =ᵐ[μ] 0 := by @@ -588,22 +569,17 @@ theorem conj_q_lt_top'_of_ae_eq_zero (g : Lp ℝ q μ) unfold conj_q_lt_top' simp_all apply measure_mono_null - . show _ ⊆ {a | ¬g a = 0} - simp_all - . apply ae_iff.mp hg + . show _ ⊆ {a | ¬g a = 0}; simp_all + . exact ae_iff.mp hg theorem conj_q_lt_top'_of_eq_zero (g : Lp ℝ q μ) (hg : g = 0) (hq₁ : q > 1) (hqᵢ : q ≠ ∞) : conj_q_lt_top' g =ᵐ[μ] 0 := by - have : g =ᵐ[μ] 0 := by - apply eq_zero_iff_ae_eq_zero.mp - exact hg + have : g =ᵐ[μ] 0 := eq_zero_iff_ae_eq_zero.mp hg exact conj_q_lt_top'_of_ae_eq_zero g this hq₁ hqᵢ theorem conj_q_lt_top'_of_nnnorm_zero (g : Lp ℝ q μ) (hg : ‖g‖₊ = 0) (hq₁ : q > 1) (hqᵢ : q ≠ ∞) : conj_q_lt_top' ↑g =ᵐ[μ] 0 := by - have : g = 0 := by - apply (nnnorm_eq_zero_iff q_gt_zero).mp - exact hg + have : g = 0 := (nnnorm_eq_zero_iff q_gt_zero).mp hg exact conj_q_lt_top'_of_eq_zero g this hq₁ hqᵢ @[simp] @@ -666,34 +642,28 @@ theorem snorm'_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) @[simp] theorem snorm_of_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : snorm (conj_q_lt_top' g) p μ = (snorm g q μ) ^ (q.toReal - 1) := by - rw[snorm_eq_snorm', snorm_eq_snorm'] - apply _root_.trans - exact snorm'_of_conj_q_lt_top' (p := p) (q := q) (hqᵢ) g - rfl - exact q_ne_zero (p := p) - exact hqᵢ - exact p_ne_zero (q := q) - exact p_ne_top + rw [snorm_eq_snorm', snorm_eq_snorm'] + · exact _root_.trans (snorm'_of_conj_q_lt_top' (p := p) (q := q) (hqᵢ) g) rfl + · exact q_ne_zero (p := p) + · exact hqᵢ + · exact p_ne_zero (q := q) + · exact p_ne_top theorem Memℒp_conj_q_lt_top' (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Memℒp (conj_q_lt_top' g) p μ := by constructor . measurability . rw[snorm_of_conj_q_lt_top' hqᵢ g] - apply ENNReal.rpow_lt_top_of_nonneg - . exact q_sub_one_nneg' (p := p) hqᵢ - . exact snorm_ne_top g + exact ENNReal.rpow_lt_top_of_nonneg (q_sub_one_nneg' (p := p) hqᵢ) (snorm_ne_top g) -def conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Lp ℝ p μ := by - apply toLp (conj_q_lt_top' g) - exact Memℒp_conj_q_lt_top' hqᵢ g +def conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : Lp ℝ p μ := + toLp (conj_q_lt_top' g) (Memℒp_conj_q_lt_top' hqᵢ g) @[simp] theorem snorm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) : snorm (conj_q_lt_top (p := p) hqᵢ g) p μ = (snorm g q μ) ^ (q.toReal - 1) := by apply _root_.trans; show _ = snorm (conj_q_lt_top' g) p μ; swap - exact snorm_of_conj_q_lt_top' hqᵢ g - apply snorm_congr_ae - apply coeFn_toLp + · exact snorm_of_conj_q_lt_top' hqᵢ g + · exact snorm_congr_ae (coeFn_toLp _ ) @[simp] theorem norm_of_conj_q_lt_top (hqᵢ : q ≠ ∞) (g : Lp ℝ q μ) @@ -717,15 +687,13 @@ def normalized_conj_q_lt_top' {q : ℝ≥0∞} (g : Lp ℝ q μ) : α → ℝ := theorem normalized_conj_q_lt_top'_ae_measurable (g : Lp ℝ q μ) : AEMeasurable (normalized_conj_q_lt_top' g) μ := by unfold normalized_conj_q_lt_top' - apply AEMeasurable.mul_const - exact conj_q_lt_top'_aemeasurable g + exact AEMeasurable.mul_const (conj_q_lt_top'_aemeasurable g) _ @[measurability] theorem normalized_conj_q_lt_top'_aestrongly_measurable (g : Lp ℝ q μ) : AEStronglyMeasurable (normalized_conj_q_lt_top' g) μ := by unfold normalized_conj_q_lt_top' - apply (aestronglyMeasurable_iff_aemeasurable (μ := μ)).mpr - exact normalized_conj_q_lt_top'_ae_measurable g + exact (aestronglyMeasurable_iff_aemeasurable (μ := μ)).mpr (normalized_conj_q_lt_top'_ae_measurable g) @[simp] theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) (hg : ‖g‖₊ ≠ 0) @@ -762,10 +730,7 @@ theorem snorm'_normalized_conj_q_lt_top' {g : Lp ℝ q μ} (hqᵢ : q ≠ ∞) ( _ = ‖g‖₊ := by rw[nnnorm_def] _ ≠ 0 := by apply ENNReal.coe_ne_zero.mpr; exact hg - have x_rpow_y_ne_top : x^y ≠ ∞ := by - apply ENNReal.rpow_ne_top_of_nonneg - exact y_nneg - exact x_ne_top + have x_rpow_y_ne_top : x^y ≠ ∞ := ENNReal.rpow_ne_top_of_nonneg y_nneg x_ne_top rw[←ENNReal.coe_toNNReal (a := x ^ y) x_rpow_y_ne_top, ENNReal.toReal_rpow, @@ -794,18 +759,16 @@ theorem Memℒp_normalized_conj_q_lt_top' (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} . rw[snorm_normalized_conj_q_lt_top' hqᵢ hg] trivial -def normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : Lp ℝ p μ := by - apply toLp (normalized_conj_q_lt_top' g) - exact Memℒp_normalized_conj_q_lt_top' hqᵢ hg +def normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : Lp ℝ p μ := + toLp (normalized_conj_q_lt_top' g) (Memℒp_normalized_conj_q_lt_top' hqᵢ hg) @[simp] theorem snorm_normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0) : snorm (normalized_conj_q_lt_top (p := p) hqᵢ hg) p μ = 1 := by apply _root_.trans show _ = snorm (normalized_conj_q_lt_top' g) p μ; swap - exact snorm_normalized_conj_q_lt_top' hqᵢ hg - apply snorm_congr_ae - apply coeFn_toLp + · exact snorm_normalized_conj_q_lt_top' hqᵢ hg + · exact snorm_congr_ae (coeFn_toLp _) @[simp] theorem norm_of_normalized_conj_q_lt_top (hqᵢ : q ≠ ∞) {g : Lp ℝ q μ} (hg : ‖g‖₊ ≠ 0)