OAI/Analysis/AncientFlat/Energy/EnergyQuadratic.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ParametrixUniqueness.massline 10 - def
OAI.ParametrixUniqueness.crossline 11 - def
OAI.ParametrixUniqueness.pairline 12 - lemma
OAI.ParametrixUniqueness.integrable_massline 13 - lemma
OAI.ParametrixUniqueness.integrable_crossline 17 - lemma
OAI.ParametrixUniqueness.integrable_pairline 21 - lemma
OAI.ParametrixUniqueness.mass_nonnegline 25 - lemma
OAI.ParametrixUniqueness.cross_nonnegline 27 - lemma
OAI.ParametrixUniqueness.weighted_youngline 29 - lemma
OAI.ParametrixUniqueness.abs_coeff_pair_leline 52 - lemma
OAI.ParametrixUniqueness.abs_pair_leline 71