OAI/Analysis/VlasovMaxwell/Regularity/NormalisedPartialCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RVM.PhaseFlowOn.labelConeKernel_triangle_norm_localBorel line 40
2. def OAI.RVM.normalisedPartialCutoff line 65
3. lemma OAI.RVM.PhaseFlowOn.normalisedPartialCutoff_continuousOn line 70
4. lemma OAI.RVM.PhaseFlowOn.partialCutoffLabelCost_eq_normalised line 83
5. lemma OAI.RVM.localBorel_clm_apply line 101
6. lemma OAI.RVM.PhaseFlowOn.partialCutoffLabelCost_multiplier_polar line 115
7. lemma OAI.RVM.product_le_min_scale line 135
8. lemma OAI.RVM.sqrt_div_stabilityLength line 144
9. lemma OAI.RVM.direction_baseline_R_bound line 153
10. lemma OAI.RVM.direction_baseline_R_log_bound line 191