OAI/Analysis/AncientFlat/Energy/EnergyProducts.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ParametrixUniqueness.Decays.const_smulline 12 - lemma
OAI.ParametrixUniqueness.dir_dir_smulline 19 - lemma
OAI.ParametrixUniqueness.decays_dir_smulline 34 - lemma
OAI.ParametrixUniqueness.decays_dir_dir_smulline 40 - lemma
OAI.ParametrixUniqueness.decays_dir_dir_weight_mulline 47 - lemma
OAI.ParametrixUniqueness.norm_dir_leline 52 - lemma
OAI.ParametrixUniqueness.norm_dir_dir_leline 56 - lemma
OAI.ParametrixUniqueness.weight_mul_boundsline 66 - lemma
OAI.ParametrixUniqueness.integral_inner_dir_dirline 120