fpvandoorn/carleson
Source indexedtheorem Β· leanprover/lean4:v4.32.0
RCLike.induction
Carleson.ToMathlib.Analysis.RCLike.Components Β· Carleson/ToMathlib/Analysis/RCLike/Components.lean:217 to 301
Mathematical statement
Exact Lean statement
theorem induction {Ξ± : Type*} {π : Type*} [RCLike π]
{Ξ² : Type*} [Mul Ξ²] {a b}
{P : (Ξ± β π) β Prop}
(P_add : β {f g : Ξ± β π}, P f β P g β P (f + g))
(P_components : β {f : Ξ± β π} {c : π} (_ : c β RCLike.Components),
P f β P (algebraMap β π β NNReal.toReal β RCLike.component c β f))
(P_mul_unit : β {f : Ξ± β π} {c : π} (_ : c β RCLike.Components), P f β P (c β’ f))
{motive : (Ξ± β π) β Ξ² β Prop}
(motive_nnreal : β {f : Ξ± β ββ₯0} (_ : P (algebraMap β π β NNReal.toReal β f)),
motive (algebraMap β π β NNReal.toReal β f) a)
(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))
(motive_mul_unit : β {f : Ξ± β π} {c : π} {n : Ξ²} (_ : c β RCLike.Components) (_ : P f),
motive f n β motive (c β’ f) n)
β¦f : Ξ± β πβ¦ (hf : P f) :
motive f (a * b * b)Complete declaration
Lean source
Full Lean sourceLean 4
theorem induction {Ξ± : Type*} {π : Type*} [RCLike π] {Ξ² : Type*} [Mul Ξ²] {a b} {P : (Ξ± β π) β Prop} (P_add : β {f g : Ξ± β π}, P f β P g β P (f + g)) (P_components : β {f : Ξ± β π} {c : π} (_ : c β RCLike.Components), P f β P (algebraMap β π β NNReal.toReal β RCLike.component c β f)) (P_mul_unit : β {f : Ξ± β π} {c : π} (_ : c β RCLike.Components), P f β P (c β’ f)) {motive : (Ξ± β π) β Ξ² β Prop} (motive_nnreal : β {f : Ξ± β ββ₯0} (_ : P (algebraMap β π β NNReal.toReal β f)), motive (algebraMap β π β NNReal.toReal β f) a) (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)) (motive_mul_unit : β {f : Ξ± β π} {c : π} {n : Ξ²} (_ : c β RCLike.Components) (_ : P f), motive f n β motive (c β’ f) n) β¦f : Ξ± β πβ¦ (hf : P f) : motive f (a * b * b) := by have f_decomposition : (1 : π) β’ ((algebraMap β π) β toReal β component 1 β f) + (-1 : π) β’ ((algebraMap β π) β toReal β component (-1) β f) + (RCLike.I : π) β’ ((algebraMap β π) β toReal β component RCLike.I β f) + (-RCLike.I : π) β’ ((algebraMap β π) β toReal β component (-RCLike.I) β f) = f := by ext x simp only [Pi.add_apply, Function.comp_apply, Pi.smul_apply, smul_eq_mul] exact RCLike.decomposition -- Decompose f into real and imaginary parts, each further split into positive/negative parts rw [β f_decomposition, add_assoc] have hP_comp : β {c : π} (_ : c β Components), P (c β’ ((algebraMap β π) β toReal β component c β f)) := fun hc => P_mul_unit hc (P_components hc hf) -- Pointwise version of the decomposition have f_decomp_pt : β x, (algebraMap β π) ((component 1 (f x)).toReal) + (-1) * (algebraMap β π) ((component (-1) (f x)).toReal) + (RCLike.I * (algebraMap β π) ((component RCLike.I (f x)).toReal) + -RCLike.I * (algebraMap β π) ((component (-RCLike.I) (f x)).toReal)) = f x := by intro x have := congr_fun f_decomposition x simp only [Pi.add_apply, Function.comp_apply, Pi.smul_apply, smul_eq_mul, one_mul] at this rw [add_assoc] at this; exact this -- Outer split: real part vs imaginary part apply motive_add' Β· -- βreal_part xβ β€ β(real_part + imag_part) xβ intro x simp only [Pi.add_apply, Function.comp_apply, Pi.smul_apply, smul_eq_mul, one_mul] rw [f_decomp_pt] exact norm_realPart_le (f x) Β· -- βimag_part xβ β€ β(real_part + imag_part) xβ intro x simp only [Pi.add_apply, Function.comp_apply, Pi.smul_apply, smul_eq_mul, one_mul] rw [f_decomp_pt] exact norm_imPart_le (f x) Β· exact P_add (hP_comp (by unfold Components; simp)) (hP_comp (by unfold Components; simp)) Β· exact P_add (hP_comp (by unfold Components; simp)) (hP_comp (by unfold Components; simp)) Β· -- Inner split: positive real vs negative real apply motive_add' Β· -- β1 * pos_re xβ β€ β(1 * pos_re + (-1) * neg_re) xβ intro x simp only [Function.comp_apply, Pi.smul_apply, smul_eq_mul, one_mul] exact norm_posReal_le (f x) Β· -- β(-1) * neg_re xβ β€ β(1 * pos_re + (-1) * neg_re) xβ intro x simp only [Function.comp_apply, Pi.smul_apply, smul_eq_mul, one_mul] exact norm_negReal_le (f x) Β· exact hP_comp (by unfold Components; simp) Β· exact hP_comp (by unfold Components; simp) Β· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf) (motive_nnreal (P_components (by unfold Components; simp) hf)) Β· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf) (motive_nnreal (P_components (by unfold Components; simp) hf)) Β· -- Inner split: positive imaginary vs negative imaginary apply motive_add' Β· -- βI * pos_im xβ β€ β(I * pos_im + (-I) * neg_im) xβ intro x simp only [Function.comp_apply, Pi.smul_apply, smul_eq_mul] exact norm_posIm_le (f x) Β· -- β(-I) * neg_im xβ β€ β(I * pos_im + (-I) * neg_im) xβ intro x simp only [Function.comp_apply, Pi.smul_apply, smul_eq_mul] exact norm_negIm_le (f x) Β· exact hP_comp (by unfold Components; simp) Β· exact hP_comp (by unfold Components; simp) Β· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf) (motive_nnreal (P_components (by unfold Components; simp) hf)) Β· exact motive_mul_unit (by unfold Components; simp) (P_components (by unfold Components; simp) hf) (motive_nnreal (P_components (by unfold Components; simp) hf))