Skip to content

Commit

Permalink
Update Dual.lean (#33)
Browse files Browse the repository at this point in the history
  • Loading branch information
@pitmonticone
pitmonticone authored Jul 6, 2024
1 parent c3102b2 commit aa19e15
Showing 1 changed file with 75 additions and 112 deletions.
187 changes: 75 additions & 112 deletions BonnAnalysis/Dual.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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 μ) :
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -247,72 +246,61 @@ 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ᵢ]

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

Expand All @@ -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

Expand Down Expand Up @@ -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'

Expand Down Expand Up @@ -567,43 +553,33 @@ 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
apply ae_iff.mpr
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]
Expand Down Expand Up @@ -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 μ)
Expand All @@ -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)
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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)
Expand Down

0 comments on commit aa19e15

Please sign in to comment.