Skip to content

Commit 6251104

Browse files
madeve-unipiAristotle-Harmonic
madeve-unipi
and
Aristotle-Harmonic
authored
Proved RCLike.induction with Aristotle (#539)
Proved RCLike.induction with Aristotle. It automatically added some private helper lemmas. Feel free to remove the comments from the proof, I left them since it (probably) makes it more readable. I also removed names from two hypotheses since the linter was complaining. Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun> Co-authored-by: Aristotle (Harmonic) <aristotle-harmonic@harmonic.fun>
1 parent fa053d3 commit 6251104

File tree

1 file changed

+166
-45
lines changed

1 file changed

+166
-45
lines changed

‎Carleson/ToMathlib/LorentzType.lean‎

Lines changed: 166 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -624,6 +624,112 @@ theorem vector_valued_induction {β γ} [AddCommMonoid β] [AddCommMonoid γ]
624624
motive 1 f := sorry
625625
-/
626626

627+
/-! ### Helper lemmas for the RCLike component decomposition norm bounds -/
628+
629+
section RCLikeComponentHelpers
630+
631+
open _root_.RCLike RCLike in
632+
private lemma component_one_add_neg_one {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
633+
algebraMap ℝ 𝕂 (component 1 a).toReal +
634+
(-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal = algebraMap ℝ 𝕂 (re a) := by
635+
unfold component
636+
simp only [map_one, mul_one, map_neg, mul_neg, neg_mul, one_mul]
637+
rw [← map_neg, ← map_add]; congr 1
638+
simp only [Real.coe_toNNReal']
639+
linarith [max_zero_sub_eq_self (re a)]
640+
641+
open _root_.RCLike RCLike in
642+
private lemma component_I_add_neg_I {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
643+
(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal +
644+
(-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal = algebraMap ℝ 𝕂 (im a) * I := by
645+
unfold component
646+
simp only [conj_I, mul_neg, Real.coe_toNNReal', map_neg]
647+
ring_nf
648+
rw [← mul_sub, ← map_sub,
649+
show max (-re (I * a)) 0 - max (re (I * a)) 0 = im a from by
650+
rw [show re (I * a) = -im a from by simp [mul_re, I_re], neg_neg]
651+
exact max_zero_sub_eq_self _]
652+
653+
open _root_.RCLike RCLike in
654+
/-- Norm of the real component part is at most `‖a‖`. -/
655+
private lemma norm_realPart_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
656+
‖algebraMap ℝ 𝕂 (component 1 a).toReal +
657+
(-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ ≤ ‖a‖ := by
658+
rw [component_one_add_neg_one, norm_ofReal]
659+
exact abs_re_le_norm a
660+
661+
open _root_.RCLike RCLike in
662+
/-- Norm of the imaginary component part is at most `‖a‖`. -/
663+
private lemma norm_imPart_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
664+
‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal +
665+
(-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ ≤ ‖a‖ := by
666+
rw [component_I_add_neg_I]
667+
calc ‖algebraMap ℝ 𝕂 (im a) * I‖
668+
≤ ‖algebraMap ℝ 𝕂 (im a)‖ * ‖(I : 𝕂)‖ := norm_mul_le _ _
669+
_ ≤ |im a| * 1 := by
670+
gcongr
671+
· exact (norm_ofReal _).le
672+
· rw [RCLike.norm_I]; split_ifs <;> simp
673+
_ = |im a| := mul_one _
674+
_ ≤ ‖a‖ := abs_im_le_norm a
675+
676+
open _root_.RCLike RCLike in
677+
/-- `max(re a, 0)` embedded in 𝕂 has norm at most `|re a|`. -/
678+
private lemma norm_posReal_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
679+
‖(algebraMap ℝ 𝕂 (component 1 a).toReal : 𝕂)‖ ≤
680+
‖algebraMap ℝ 𝕂 (component 1 a).toReal +
681+
(-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ := by
682+
rw [component_one_add_neg_one, norm_ofReal, norm_ofReal]
683+
unfold component
684+
simp only [map_one, mul_one, Real.coe_toNNReal']
685+
rw [abs_of_nonneg (le_max_right _ _)]
686+
exact max_le (le_abs_self _) (abs_nonneg _)
687+
688+
open _root_.RCLike RCLike in
689+
/-- `max(-re a, 0)` negated and embedded in 𝕂 has norm at most `|re a|`. -/
690+
private lemma norm_negReal_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
691+
‖(-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ ≤
692+
‖algebraMap ℝ 𝕂 (component 1 a).toReal +
693+
(-1 : 𝕂) * algebraMap ℝ 𝕂 (component (-1) a).toReal‖ := by
694+
rw [component_one_add_neg_one, norm_ofReal]
695+
simp only [neg_mul, one_mul, norm_neg, norm_ofReal]
696+
unfold component
697+
simp only [map_neg, map_one, mul_neg, mul_one, Real.coe_toNNReal']
698+
rw [abs_of_nonneg (le_max_right _ _)]
699+
simp [abs_nonneg, neg_le_abs]
700+
701+
open _root_.RCLike RCLike in
702+
/-- `I * max(im a, 0)` has norm at most `‖I * im⁺ - I * im⁻‖`. -/
703+
private lemma norm_posIm_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
704+
‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal‖ ≤
705+
‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal +
706+
(-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ := by
707+
rw [component_I_add_neg_I, norm_mul, norm_mul, norm_ofReal, norm_ofReal,
708+
mul_comm (‖(I : 𝕂)‖)]
709+
apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
710+
unfold component
711+
simp only [conj_I, mul_neg, Real.coe_toNNReal']
712+
change |max (re (-(a * I))) 0| ≤ |im a|
713+
rw [show re (-(a * I)) = im a from by simp [mul_re, I_re, I_im]]
714+
simp [abs_of_nonneg, le_abs_self]
715+
716+
open _root_.RCLike RCLike in
717+
/-- `-I * max(-im a, 0)` has norm at most `‖I * im⁺ - I * im⁻‖`. -/
718+
private lemma norm_negIm_le {𝕂 : Type*} [RCLike 𝕂] (a : 𝕂) :
719+
‖(-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ ≤
720+
‖(I : 𝕂) * algebraMap ℝ 𝕂 (component I a).toReal +
721+
(-I : 𝕂) * algebraMap ℝ 𝕂 (component (-I) a).toReal‖ := by
722+
rw [component_I_add_neg_I]
723+
simp only [norm_neg, norm_mul, norm_ofReal, mul_comm (‖(I : 𝕂)‖)]
724+
apply mul_le_mul_of_nonneg_right _ (norm_nonneg _)
725+
unfold component
726+
simp only [map_neg, conj_I, neg_neg, Real.coe_toNNReal']
727+
rw [show re (a * I) = -im a from by simp [mul_re, I_re, I_im]]
728+
rw [abs_of_nonneg (le_max_right _ _)]
729+
exact max_le (neg_le_abs _) (abs_nonneg _)
730+
731+
end RCLikeComponentHelpers
732+
627733
--TODO: clean up the proof
628734
theorem RCLike.induction {𝕂 : Type*} [RCLike 𝕂]
629735
{β : Type*} [Mul β] {a b}
@@ -635,7 +741,7 @@ theorem RCLike.induction {𝕂 : Type*} [RCLike 𝕂]
635741
{motive : (α → 𝕂) → β → Prop}
636742
(motive_nnreal : ∀ {f : α → ℝ≥0} (_ : P (algebraMap ℝ 𝕂 ∘ NNReal.toReal ∘ f)),
637743
motive (algebraMap ℝ 𝕂 ∘ NNReal.toReal ∘ f) a)
638-
(motive_add' : ∀ {n : β} {f g : α → 𝕂} (hf_add : ∀ {x}, ‖f x‖ ≤ ‖f x + g x‖) (hg_add : ∀ {x}, ‖g x‖ ≤ ‖f x + g x‖) (_ : P f) (_ : P g), motive f n → motive g n → motive (f + g) (n * b))
744+
(motive_add' : ∀ {n : β} {f g : α → 𝕂} (_ : ∀ {x}, ‖f x‖ ≤ ‖f x + g x‖) (_ : ∀ {x}, ‖g x‖ ≤ ‖f x + g x‖) (_ : P f) (_ : P g), motive f n → motive g n → motive (f + g) (n * b))
639745
(motive_mul_unit : ∀ {f : α → 𝕂} {c : 𝕂} {n : β} (_ : c ∈ RCLike.Components) (_ : P f),
640746
motive f n → motive (c • f) n)
641747
⦃f : α → 𝕂⦄ (hf : P f) :
@@ -648,51 +754,66 @@ theorem RCLike.induction {𝕂 : Type*} [RCLike 𝕂]
648754
ext x
649755
simp only [Pi.add_apply, comp_apply, Pi.smul_apply, smul_eq_mul]
650756
exact RCLike.decomposition
651-
rw [← f_decomposition]
652-
rw [add_assoc]
757+
-- Decompose f into real and imaginary parts, each further split into positive/negative parts
758+
rw [← f_decomposition, add_assoc]
759+
have hP_comp : ∀ {c : 𝕂} (_ : c ∈ Components),
760+
P (c • ((algebraMap ℝ 𝕂) ∘ toReal ∘ component c ∘ f)) := fun hc =>
761+
P_mul_unit hc (P_components hc hf)
762+
-- Pointwise version of the decomposition
763+
have f_decomp_pt : ∀ x, (algebraMap ℝ 𝕂) ((component 1 (f x)).toReal)
764+
+ (-1) * (algebraMap ℝ 𝕂) ((component (-1) (f x)).toReal)
765+
+ (RCLike.I * (algebraMap ℝ 𝕂) ((component RCLike.I (f x)).toReal)
766+
+ -RCLike.I * (algebraMap ℝ 𝕂) ((component (-RCLike.I) (f x)).toReal)) = f x := by
767+
intro x
768+
have := congr_fun f_decomposition x
769+
simp only [Pi.add_apply, comp_apply, Pi.smul_apply, smul_eq_mul, one_mul] at this
770+
rw [add_assoc] at this; exact this
771+
-- Outer split: real part vs imaginary part
653772
apply motive_add'
654-
· sorry
655-
· sorry
656-
· apply P_add
657-
· apply P_mul_unit (by unfold Components; simp)
658-
apply P_components (by unfold Components; simp) hf
659-
· apply P_mul_unit (by unfold Components; simp)
660-
apply P_components (by unfold Components; simp) hf
661-
· apply P_add
662-
· apply P_mul_unit (by unfold Components; simp)
663-
apply P_components (by unfold Components; simp) hf
664-
· apply P_mul_unit (by unfold Components; simp)
665-
apply P_components (by unfold Components; simp) hf
666-
· apply motive_add'
667-
· sorry
668-
· sorry
669-
· apply P_mul_unit (by unfold Components; simp)
670-
apply P_components (by unfold Components; simp) hf
671-
· apply P_mul_unit (by unfold Components; simp)
672-
apply P_components (by unfold Components; simp) hf
673-
· apply motive_mul_unit (by unfold Components; simp)
674-
· apply P_components (by unfold Components; simp) hf
675-
apply motive_nnreal (f := component _ ∘ f)
676-
apply P_components (by unfold Components; simp) hf
677-
· apply motive_mul_unit (by unfold Components; simp)
678-
· apply P_components (by unfold Components; simp) hf
679-
apply motive_nnreal (f := component _ ∘ f)
680-
apply P_components (by unfold Components; simp) hf
681-
· apply motive_add'
682-
· sorry
683-
· sorry
684-
· apply P_mul_unit (by unfold Components; simp)
685-
apply P_components (by unfold Components; simp) hf
686-
· apply P_mul_unit (by unfold Components; simp)
687-
apply P_components (by unfold Components; simp) hf
688-
· apply motive_mul_unit (by unfold Components; simp)
689-
· apply P_components (by unfold Components; simp) hf
690-
apply motive_nnreal (f := component _ ∘ f)
691-
apply P_components (by unfold Components; simp) hf
692-
· apply motive_mul_unit (by unfold Components; simp)
693-
· apply P_components (by unfold Components; simp) hf
694-
apply motive_nnreal (f := component _ ∘ f)
695-
apply P_components (by unfold Components; simp) hf
773+
· -- ‖real_part x‖ ≤ ‖(real_part + imag_part) x‖
774+
intro x
775+
simp only [Pi.add_apply, comp_apply, Pi.smul_apply, smul_eq_mul, one_mul]
776+
rw [f_decomp_pt]
777+
exact norm_realPart_le (f x)
778+
· -- ‖imag_part x‖ ≤ ‖(real_part + imag_part) x‖
779+
intro x
780+
simp only [Pi.add_apply, comp_apply, Pi.smul_apply, smul_eq_mul, one_mul]
781+
rw [f_decomp_pt]
782+
exact norm_imPart_le (f x)
783+
· exact P_add (hP_comp (by unfold Components; simp)) (hP_comp (by unfold Components; simp))
784+
· exact P_add (hP_comp (by unfold Components; simp)) (hP_comp (by unfold Components; simp))
785+
· -- Inner split: positive real vs negative real
786+
apply motive_add'
787+
· -- ‖1 * pos_re x‖ ≤ ‖(1 * pos_re + (-1) * neg_re) x‖
788+
intro x
789+
simp only [comp_apply, Pi.smul_apply, smul_eq_mul, one_mul]
790+
exact norm_posReal_le (f x)
791+
· -- ‖(-1) * neg_re x‖ ≤ ‖(1 * pos_re + (-1) * neg_re) x‖
792+
intro x
793+
simp only [comp_apply, Pi.smul_apply, smul_eq_mul, one_mul]
794+
exact norm_negReal_le (f x)
795+
· exact hP_comp (by unfold Components; simp)
796+
· exact hP_comp (by unfold Components; simp)
797+
· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf)
798+
(motive_nnreal (P_components (by unfold Components; simp) hf))
799+
· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf)
800+
(motive_nnreal (P_components (by unfold Components; simp) hf))
801+
· -- Inner split: positive imaginary vs negative imaginary
802+
apply motive_add'
803+
· -- ‖I * pos_im x‖ ≤ ‖(I * pos_im + (-I) * neg_im) x‖
804+
intro x
805+
simp only [comp_apply, Pi.smul_apply, smul_eq_mul]
806+
exact norm_posIm_le (f x)
807+
· -- ‖(-I) * neg_im x‖ ≤ ‖(I * pos_im + (-I) * neg_im) x‖
808+
intro x
809+
simp only [comp_apply, Pi.smul_apply, smul_eq_mul]
810+
exact norm_negIm_le (f x)
811+
· exact hP_comp (by unfold Components; simp)
812+
· exact hP_comp (by unfold Components; simp)
813+
· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf)
814+
(motive_nnreal (P_components (by unfold Components; simp) hf))
815+
· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf)
816+
(motive_nnreal (P_components (by unfold Components; simp) hf))
696817

697818
theorem enorm_eq_enorm_embedRCLike {𝕂 : Type*} [RCLike 𝕂] {f : α → ℝ≥0} (x : α) :
698819
‖(⇑(algebraMap ℝ 𝕂) ∘ toReal ∘ f) x‖ₑ = ‖f x‖ₑ := by

0 commit comments

Comments
 (0)
⚡