OAI/Analysis/Conductivity/Sobolev/CompactUpdateLp.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.voltageGradient_sum line 13
2. lemma OAI.ScalarConductivity.CompactGlobalUpdate.gradient_mean_zero_restrict line 21
3. lemma OAI.ScalarConductivity.CompactGlobalUpdate.flux_mean_zero_restrict line 31
4. lemma OAI.ScalarConductivity.CompactGlobalUpdate.memLp_gradient_correction line 42
5. lemma OAI.ScalarConductivity.CompactGlobalUpdate.memLp_flux_correction line 49
6. lemma OAI.ScalarConductivity.CompactGlobalUpdate.gradient_toLp_eq line 56
7. lemma OAI.ScalarConductivity.CompactGlobalUpdate.flux_toLp_eq line 67
8. lemma OAI.ScalarConductivity.norm_correction_bound_of_add line 79
9. lemma OAI.ScalarConductivity.CompactGlobalUpdate.correction_energy_bound line 86