OAI/Analysis/NefAdjoint/FractionalDensity.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Local fractional-density integrability

Simple normal-crossing densities with coefficients strictly less than one are locally integrable. Rational fractional coefficients admit a common exponent a > 1, giving the local L^a input to Hölder's inequality in the weight-integral bounds. Supporting results cover interpolation and floor arithmetic, logarithmic comparison weights, contraction, and fixed-space weak convergence and class vanishing.

This local coordinate result omits the bounded geometric factor, coordinate gluing, regularized metric bounds, and the uniform integral estimate. It establishes neither a geometric adjoint-metric theorem nor injectivity of the natural coherent-cohomology inclusion. NefAdjoint.SNC.LelongSNCDivergenceGoal remains a goal proposition, not a proved theorem.

  1. def OAI.NefAdjoint.SNC.euclideanNorm line 26
  2. def OAI.NefAdjoint.SNC.boundaryWeight line 27
  3. def OAI.NefAdjoint.SNC.density line 29
  4. def OAI.NefAdjoint.SNC.SNCDensityGoal line 32
  5. def OAI.NefAdjoint.SNC.LelongSNCDivergenceGoal line 35
  6. def OAI.NefAdjoint.SNC.powerDensity line 54
  7. lemma OAI.NefAdjoint.SNC.powerDensity_nonneg line 57
  8. lemma OAI.NefAdjoint.SNC.density_eq_power line 60
  9. lemma OAI.NefAdjoint.SNC.density_ae_power line 69
  10. lemma OAI.NefAdjoint.SNC.planar_power_integrable line 74
  11. lemma OAI.NefAdjoint.SNC.powerDensity_integrable_polydisc line 85
  12. lemma OAI.NefAdjoint.SNC.powerDensity_locallyIntegrable line 93
  13. theorem OAI.NefAdjoint.SNC.snc_density line 102
  14. def OAI.NefAdjoint.InteriorBoundary.interpolate line 114
  15. def OAI.NefAdjoint.InteriorBoundary.floorDifference line 117
  16. lemma OAI.NefAdjoint.InteriorBoundary.interpolate_between line 120
  17. lemma OAI.NefAdjoint.InteriorBoundary.floorDifference_nonneg line 128
  18. lemma OAI.NefAdjoint.InteriorBoundary.adjoint_difference line 133
  19. lemma OAI.NefAdjoint.InteriorBoundary.interpolate_ne_zero_iff line 140
  20. lemma OAI.NefAdjoint.InteriorBoundary.exists_common_exponent line 157
  21. lemma OAI.NefAdjoint.InteriorBoundary.fractional_coefficients line 169
  22. lemma OAI.NefAdjoint.SNC.density_rpow line 181
  23. theorem OAI.NefAdjoint.SNC.exists_locallyIntegrable_power line 188
  24. lemma OAI.NefAdjoint.SNC.fractional_density_power line 196
  25. def OAI.NefAdjoint.ComparisonWeights.logSum line 206
  26. lemma OAI.NefAdjoint.ComparisonWeights.le_logSum_left line 208
  27. lemma OAI.NefAdjoint.ComparisonWeights.le_logSum_right line 214
  28. lemma OAI.NefAdjoint.ComparisonWeights.logSum_add line 218
  29. lemma OAI.NefAdjoint.ComparisonWeights.logSum_le_of_le line 223
  30. lemma OAI.NefAdjoint.ComparisonWeights.raised_exponential_le line 228
  31. lemma OAI.NefAdjoint.ComparisonWeights.integral_weight_contraction line 233
  32. theorem OAI.NefAdjoint.FixedSpace.tendsto_pairings_of_dense line 251
  33. theorem OAI.NefAdjoint.FixedSpace.tendsto_duals_of_dense line 283
  34. theorem OAI.NefAdjoint.FixedSpace.constant_class_vanishes line 292
  35. theorem OAI.NefAdjoint.FixedSpace.class_vanishes_of_weakly_null_differences line 305
  36. theorem OAI.NefAdjoint.FixedSpace.class_vanishes_of_closure_differences line 317