OAI/Combinatorics/HoneycombChords/ControlledTransforms.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Exponential control, differentiation under the integral, and fusion identities.

The development follows OpenAI, Uniform marked-polygon estimates and sharp finite bridge moments (2026), Sections 6 and 7.

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.sinh_le_mul_exp line 16
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zG_norm_le line 23
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.power_le_one_add line 30
  4. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.ControlledDensity line 37
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.ControlledDensity.zero line 41
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.ControlledDensity.add line 44
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.ControlledDensity.smul line 52
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zMonomial_controlled line 60
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zCoshJet_controlled line 69
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zG_controlled line 78
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zDensity_controlled line 85
  12. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedJet line 108
  13. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedIntegral line 110
  14. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.jetBound line 112
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedJet_zero line 115
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedIntegral_zero line 117
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedJet_hasDerivAt line 120
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedJet_measurable line 132
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.jetBound_integrable line 137
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedJet_norm_le line 147
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedJet_integrable line 168
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedIntegral_hasDerivAt line 177
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.weightedIntegral_iteratedDeriv line 197
  24. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zD line 221
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zD_norm_le line 223
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.ControlledDensity.mul_zD line 234
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zKernel_fusion line 248
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.zTransform_fusion line 255
  29. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralInterpolant line 275
  30. def OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralFusion line 277
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralInterpolant_fusion line 281
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.Analytic.integralInterpolant_fusion_eventually line 293