OAI/Geometry/TamingCompatibility/DifferentialForms/CriticalRescale.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.TamingCompatibility.HilbertSobolev.rescaleSchwartzline 21 - lemma
OAI.TamingCompatibility.HilbertSobolev.rescaleSchwartz_applyline 27 - lemma
OAI.TamingCompatibility.HilbertSobolev.rescaleSchwartz_derivativeline 32 - lemma
OAI.TamingCompatibility.HilbertSobolev.rescaleSchwartz_normline 45 - lemma
OAI.TamingCompatibility.HilbertSobolev.rescaleSchwartz_L2line 72 - lemma
OAI.TamingCompatibility.HilbertSobolev.rescaleSchwartz_L4line 85 - lemma
OAI.TamingCompatibility.HilbertSobolev.schwartz_cutoff_L2_L4line 98 - lemma
OAI.TamingCompatibility.HilbertSobolev.schwartz_cutoff_L2_L2line 114