BrunnMinkowski.lean`

GitHub source file

1804 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LogBrunnMinkowski.Space line 15
Also declared: ComparatorChallenges/LogBrunnMinkowski.lean:12 (same declaration text).
def OAI.LogBrunnMinkowski.IsConvexBody line 17
Also declared: ComparatorChallenges/LogBrunnMinkowski.lean:14 (same declaration text).
def OAI.LogBrunnMinkowski.OriginSymmetric line 20
Also declared: ComparatorChallenges/LogBrunnMinkowski.lean:17 (same declaration text).
def OAI.LogBrunnMinkowski.support line 23
Distinct definitions of this name: ComparatorChallenges/LogBrunnMinkowski.lean:20 (different declaration text). Qualify references as OAI.LogBrunnMinkowski.support@path.
def OAI.LogBrunnMinkowski.wulff line 26
Also declared: ComparatorChallenges/LogBrunnMinkowski.lean:23 (same declaration text).
def OAI.LogBrunnMinkowski.logCombination line 29
Distinct definitions of this name: ComparatorChallenges/LogBrunnMinkowski.lean:26 (different declaration text). Qualify references as OAI.LogBrunnMinkowski.logCombination@path.
def OAI.CompactMomentVariational.conjugate line 46
lemma OAI.CompactMomentVariational.values_nonempty line 49
lemma OAI.CompactMomentVariational.values_bdd line 52
lemma OAI.CompactMomentVariational.le_conjugate line 62
lemma OAI.CompactMomentVariational.conjugate_le line 67
lemma OAI.CompactMomentVariational.conjugate_upper line 73
lemma OAI.CompactMomentVariational.conjugate_nonneg line 83
lemma OAI.CompactMomentVariational.conjugate_zero line 88
lemma OAI.CompactMomentVariational.convexOn_conjugate line 94
lemma OAI.CompactMomentVariational.conjugate_sub_le line 108
lemma OAI.CompactMomentVariational.conjugate_lipschitz line 120
lemma OAI.CompactMomentVariational.conjugate_even line 133
lemma OAI.CompactMomentVariational.conjugate_coercive line 146
lemma OAI.CompactMomentVariational.convex_small_ball_bound line 169
lemma OAI.CompactMomentVariational.convex_ball_mean_bound_at line 196
lemma OAI.CompactMomentVariational.convex_ball_mean_bound line 249
lemma OAI.CompactMomentVariational.convex_ball_probability_bound line 303
lemma OAI.CompactMomentVariational.convex_ball_probability_bound_at line 321
lemma OAI.CompactMomentVariational.integrable_exp_neg_norm line 345
lemma OAI.CompactMomentVariational.integral_exp_neg_norm_scale line 366
lemma OAI.CompactMomentVariational.tail_integrable line 372
lemma OAI.CompactMomentVariational.partition_bound line 381
lemma OAI.CompactMomentVariational.log_partition_bound line 395
lemma OAI.CompactMomentVariational.ball_real_pos line 416
lemma OAI.CompactMomentVariational.mean_conjugate_lower line 424
lemma OAI.CompactMomentVariational.logarithmic_growth_bound line 450
def OAI.CompactMomentVariational.functional line 465
def OAI.CompactMomentVariational.coercivityConstant line 468
lemma OAI.CompactMomentVariational.functional_coercive line 474
lemma OAI.CompactMomentVariational.functional_lower_mean_bound line 507
def OAI.MomentCompactness.normalizedLipschitz line 528
lemma OAI.MomentCompactness.normalizedLipschitz_pointwise line 531
lemma OAI.MomentCompactness.normalizedLipschitz_compact line 541
lemma OAI.MomentCompactness.normalizedLipschitz_subsequence line 559
structure OAI.CompactMomentVariational.Admissible line 577
lemma OAI.CompactMomentVariational.conjugate_mono line 586
lemma OAI.CompactMomentVariational.mean_conjugate_lower_ball line 595
lemma OAI.CompactMomentVariational.admissible_conjugate_lipschitz line 612
lemma OAI.CompactMomentVariational.functional_coercive_ball line 618
lemma OAI.CompactMomentVariational.admissible_local_bound line 645
lemma OAI.CompactMomentVariational.uniform_conjugate_coercive line 659
structure OAI.CompactMomentVariational.NormalizedConvex line 681
lemma OAI.CompactMomentVariational.convexOn_limit line 689
lemma OAI.CompactMomentVariational.even_limit line 699
lemma OAI.CompactMomentVariational.admissible_conjugate_normalized line 709
lemma OAI.CompactMomentVariational.admissible_conjugate_subsequence line 723
lemma OAI.CompactMomentVariational.conjugate_limit_bdd line 739
lemma OAI.CompactMomentVariational.convexOn_conjugate_of_bdd line 760
lemma OAI.CompactMomentVariational.conjugate_even_univ line 776
def OAI.CompactMomentVariational.dualOn line 786
lemma OAI.CompactMomentVariational.dualOn_eq line 788
lemma OAI.CompactMomentVariational.convexOn_dualOn line 791
lemma OAI.CompactMomentVariational.dualOn_nonneg line 796
lemma OAI.CompactMomentVariational.dualOn_zero line 805
lemma OAI.CompactMomentVariational.dualOn_even_ball line 816
lemma OAI.CompactMomentVariational.fenchel_dualOn line 825
lemma OAI.CompactMomentVariational.minorant_slope_norm line 834
theorem OAI.CompactMomentVariational.conjugate_dualOn_ball line 855
lemma OAI.CompactMomentVariational.dualOn_le_liminf line 906
lemma OAI.CompactMomentVariational.dualOn_mean_lower_semicontinuous line 931
lemma OAI.CompactMomentVariational.partition_tendsto line 964
lemma OAI.CompactMomentVariational.admissible_zero line 988
lemma OAI.CompactMomentVariational.admissible_local_bounds line 993
lemma OAI.CompactMomentVariational.limit_dual_admissible line 1009
lemma OAI.CompactMomentVariational.functional_limit_upper line 1031
def OAI.CompactMomentVariational.valueSet line 1069
lemma OAI.CompactMomentVariational.maximizing_sequence line 1072
lemma OAI.CompactMomentVariational.maximizing_limit line 1108
theorem OAI.CompactMomentVariational.exists_variational_maximizer line 1125
lemma OAI.CompactMomentVariational.even_convex_minimum line 1138
lemma OAI.CompactMomentVariational.conjugate_perturb_le line 1145
lemma OAI.CompactMomentVariational.conjugate_perturb_abs line 1153
lemma OAI.CompactMomentVariational.normalized_conjugate line 1169
lemma OAI.CompactMomentVariational.normalized_conjugate_dual_bdd line 1189
lemma OAI.CompactMomentVariational.normalized_envelope_le line 1202
lemma OAI.CompactMomentVariational.normalized_envelope_admissible line 1221
lemma OAI.CompactMomentVariational.normalized_envelope_functional_ge line 1244
lemma OAI.CompactMomentVariational.fenchel_gap_control line 1289
lemma OAI.CompactMomentVariational.tilt_lower line 1329
lemma OAI.CompactMomentVariational.tilted_conjugate_remainder_bound line 1338
lemma OAI.CompactMomentVariational.hasDerivAt_conjugate_tilt line 1383
lemma OAI.CompactMomentVariational.conjugate_tilt_lipschitz line 1412
lemma OAI.CompactMomentVariational.exp_sub_bound line 1422
lemma OAI.CompactMomentVariational.tilt_density_lipschitz line 1429
lemma OAI.CompactMomentVariational.hasDerivAt_tilt_partition line 1459
lemma OAI.CompactMomentVariational.tilt_partition_integrable line 1486
lemma OAI.CompactMomentVariational.measurable_gradient line 1502
lemma OAI.CompactMomentVariational.admissible_tail line 1507
lemma OAI.CompactMomentVariational.admissible_partition_integrable line 1519
lemma OAI.CompactMomentVariational.maximal_functional_tilt_le line 1526
lemma OAI.CompactMomentVariational.first_variation_even line 1543
lemma OAI.CompactMomentVariational.gradient_odd_of_even line 1588
lemma OAI.CompactMomentVariational.measure_ext_bounded_lipschitz line 1603
lemma OAI.CompactMomentVariational.first_variation_bounded line 1630
def OAI.CompactMomentVariational.normalizedSource line 1686
lemma OAI.CompactMomentVariational.normalizedSource_probability line 1690
lemma OAI.CompactMomentVariational.integral_normalizedSource line 1702
lemma OAI.CompactMomentVariational.maximizer_pushforward line 1717
theorem OAI.CompactMomentVariational.exists_weak_compact_moment line 1735
def OAI.TruncatedMoment.partition line 1762
def OAI.TruncatedMoment.target line 1765
lemma OAI.TruncatedMoment.integrable_density line 1769
lemma OAI.TruncatedMoment.partition_pos line 1774
lemma OAI.TruncatedMoment.probability line 1783
lemma OAI.TruncatedMoment.ae_mem_ball line 1796
lemma OAI.TruncatedMoment.density_lower line 1800
lemma OAI.TruncatedMoment.even_density_measure line 1824
lemma OAI.TruncatedMoment.negInvariant line 1838
lemma OAI.CompactMomentVariational.gradient_add_constant line 1857
lemma OAI.CompactMomentVariational.source_shift line 1863
theorem OAI.CompactMomentVariational.exists_weak_truncated line 1872
lemma OAI.CompactMomentVariational.convex_supporting_gradient line 1909
lemma OAI.CompactMomentVariational.fenchel_eq_at_gradient line 1925
lemma OAI.CompactMomentVariational.inverse_gradient line 1946
lemma OAI.CompactMomentVariational.locallyLipschitz_ae_differentiable line 1972
lemma OAI.CompactMomentVariational.convex_ae_differentiable line 1995
lemma OAI.CompactMomentVariational.gradient_measurable line 2001
theorem OAI.CompactMomentVariational.weak_inverse line 2004
theorem OAI.CompactMomentVariational.reverse_pushforward line 2020
lemma OAI.CompactMomentVariational.map_density_pullback line 2034
lemma OAI.CompactMomentVariational.reverse_weighted line 2044
lemma OAI.CompactMomentVariational.dual_conjugate_bdd line 2055
lemma OAI.CompactMomentVariational.dual_add_constant_bdd line 2065
theorem OAI.CompactMomentVariational.weak_MA_of_transport line 2081
theorem OAI.CompactMomentVariational.exists_weak_truncated_MA line 2124
def OAI.CompactMomentVariational.SupportingSlope line 2177
lemma OAI.CompactMomentVariational.fenchel_eq_of_support line 2181
lemma OAI.CompactMomentVariational.dual_gradient_of_support line 2198
lemma OAI.CompactMomentVariational.supportingSlope_of_localMin line 2214
theorem OAI.CompactMomentVariational.subgradient_comparison line 2230
lemma OAI.CompactMomentVariational.measure_support_image_le line 2259
theorem OAI.CompactMomentVariational.weighted_subgradient_comparison line 2277
def OAI.CompactMomentVariational.proximalEnergy line 2298
lemma OAI.CompactMomentVariational.proximal_exists line 2300
def OAI.CompactMomentVariational.proximal line 2322
lemma OAI.CompactMomentVariational.proximal_min line 2325
lemma OAI.CompactMomentVariational.support_of_proximal_min line 2330
lemma OAI.CompactMomentVariational.proximal_support line 2361
lemma OAI.CompactMomentVariational.supporting_monotone line 2366
lemma OAI.CompactMomentVariational.proximal_firm_of_support line 2375
lemma OAI.CompactMomentVariational.proximal_firm line 2383
lemma OAI.CompactMomentVariational.proximal_lipschitz line 2388
lemma OAI.CompactMomentVariational.proximal_eq_of_support line 2399
lemma OAI.CompactMomentVariational.proximal_add_slope line 2406
lemma OAI.CompactMomentVariational.gradient_eq_of_support line 2411
lemma OAI.CompactMomentVariational.norm_gradient_le_lipschitz line 2423
lemma OAI.CompactMomentVariational.gradient_continuousWithin_differentiability line 2428
lemma OAI.ConvexRegularity.lipschitz_image_null line 2462
lemma OAI.ConvexRegularity.ae_regular_preimage line 2471
theorem OAI.CompactMomentVariational.ae_gradient_differentiableWithin line 2497
lemma OAI.CompactMomentVariational.supportingSlope_limit line 2532
lemma OAI.CompactMomentVariational.exists_supportingSlope line 2546
def OAI.CompactMomentVariational.chosenSlope line 2565
lemma OAI.CompactMomentVariational.norm_chosenSlope_le line 2568
lemma OAI.CompactMomentVariational.chosenSlope_support line 2572
lemma OAI.CompactMomentVariational.chosenSlope_eq_gradient line 2576
lemma OAI.CompactMomentVariational.chosenSlope_continuousAt line 2581
theorem OAI.CompactMomentVariational.ae_chosenSlope_differentiable line 2597
lemma OAI.CompactMomentVariational.ae_gradient_hasFDerivWithin line 2618
theorem OAI.MomentJacobian.jacobian_of_ae_inverse_within line 2638
theorem OAI.CompactMomentVariational.ae_abs_det_of_weak_truncated line 2688
def OAI.CompactMomentVariational.proximalConjugate line 2733
lemma OAI.CompactMomentVariational.proximalConjugate_support line 2736
lemma OAI.CompactMomentVariational.proximalConjugate_remainder line 2747
lemma OAI.CompactMomentVariational.proximalConjugate_hasFDerivAt line 2760
lemma OAI.CompactMomentVariational.proximal_derivative_symmetric line 2769
lemma OAI.CompactMomentVariational.supporting_selection_monotone_line line 2778
lemma OAI.CompactMomentVariational.supporting_derivative_nonneg line 2791
theorem OAI.CompactMomentVariational.ae_chosenSlope_positive line 2812
def OAI.CompactMomentVariational.weakHessian line 2852
lemma OAI.CompactMomentVariational.det_weakHessian line 2856
theorem OAI.CompactMomentVariational.ae_positive_MA line 2861
lemma OAI.CompactMomentVariational.supporting_selection_injective_at line 2901
theorem OAI.CompactMomentVariational.ae_weighted_jacobian_comparison line 2940
theorem OAI.CompactMomentVariational.ae_strict_weighted_comparison line 3000
lemma OAI.CompactMomentVariational.radial_lower_of_finite_dual line 3043
lemma OAI.WeakMomentBound.ball_alignment line 3086
lemma OAI.WeakMomentBound.difference_alignment line 3095
def OAI.WeakMomentBound.secondDiff line 3107
lemma OAI.WeakMomentBound.secondDiff_nonneg line 3110
lemma OAI.WeakMomentBound.secondDiff_le_gradient line 3120
lemma OAI.WeakMomentBound.slope_alignment line 3132
theorem OAI.WeakMomentBound.secondDiff_vanishes line 3153
theorem OAI.WeakMomentBound.secondDiff_attains_max line 3211
lemma OAI.LogDetConcavity.trace_mul_nonneg line 3246
lemma OAI.LogDetConcavity.logdet_le_trace line 3254
theorem OAI.LogDetConcavity.tangent line 3264
theorem OAI.LogDetConcavity.midpoint_comparison line 3289
def OAI.WeakMomentBound.shiftedMean line 3309
def OAI.WeakMomentBound.slopeMean line 3312
lemma OAI.WeakMomentBound.slopeMean_support line 3314
lemma OAI.WeakMomentBound.shiftedMean_continuous line 3329
lemma OAI.WeakMomentBound.slopeMean_hasFDerivAt line 3334
lemma OAI.WeakMomentBound.shiftedMean_differentiableAt line 3343
lemma OAI.WeakMomentBound.inner_pos_of_matrix_posDef line 3356
lemma OAI.WeakMomentBound.mean_matrix_posDef line 3380
lemma OAI.WeakMomentBound.logdet_mean line 3383
lemma OAI.WeakMomentBound.matrix_slopeMean line 3391
lemma OAI.WeakMomentBound.finite_difference_gain line 3404
lemma OAI.WeakMomentBound.density_lt_of_logdet line 3424
theorem OAI.CompactMomentVariational.weak_secondDiff_cap line 3445
lemma OAI.QuadraticRegularity.remainder_of_secondDiff line 3564
lemma OAI.QuadraticRegularity.hasFDerivAt_of_remainder line 3578
lemma OAI.QuadraticRegularity.slope_difference_bound line 3589
lemma OAI.QuadraticRegularity.lipschitz_of_remainder line 3622
lemma OAI.QuadraticRegularity.contDiff_one_of_remainder line 3634
theorem OAI.CompactMomentVariational.weak_contDiff_one line 3653
theorem OAI.CompactMomentVariational.exists_C11_truncated line 3683
lemma OAI.SourceIdentity.norm_exp_bound line 3709
lemma OAI.SourceIdentity.integrable_norm_density line 3722
lemma OAI.SourceIdentity.gradient_moment_integrable line 3741
lemma OAI.SourceIdentity.coordinate_identity line 3755
lemma OAI.SourceIdentity.coordinate_moment_integrable line 3802
lemma OAI.SourceIdentity.euclidean_identity line 3819
lemma OAI.SourceIdentity.weighted_identity line 3838
lemma OAI.UniformMoment.supporting_plane line 3865
lemma OAI.UniformMoment.even_convex_min line 3881
lemma OAI.UniformMoment.abs_inner_le line 3889
lemma OAI.UniformMoment.first_moment_bound line 3903
lemma OAI.UniformMoment.uniform_coercivity line 3917
def OAI.UniformMoment.ballMoment line 3935
lemma OAI.UniformMoment.ballMoment_integrable line 3937
lemma OAI.UniformMoment.continuous_ballMoment line 3942
lemma OAI.UniformMoment.ballMoment_smul line 3963
lemma OAI.UniformMoment.ballMoment_pos_of_norm_one line 3967
lemma OAI.UniformMoment.exists_ballMoment_lower line 3987
lemma OAI.UniformMoment.exists_first_moment_lower line 4012
lemma OAI.UniformMoment.integrable_exp_neg_norm line 4033
lemma OAI.UniformMoment.centered_mass line 4055
lemma OAI.UniformMoment.centered_integrable line 4065
lemma OAI.UniformMoment.centered_mass_lower line 4078
lemma OAI.UniformMoment.uniform_density_majorant line 4094
lemma OAI.TruncatedMoment.uniform_density_lower line 4128
lemma OAI.CompactMomentVariational.integral_density_one line 4167
lemma OAI.CompactMomentVariational.weighted_gradient_moment_integrable line 4176
lemma OAI.CompactMomentVariational.weighted_gradient_identity line 4190
lemma OAI.CompactMomentVariational.target_first_moment_integrable line 4204
lemma OAI.CompactMomentVariational.uniform_centered_coercivity line 4213
lemma OAI.UniformMoment.centered_upper_of_secondDiff line 4244
lemma OAI.UniformMoment.gradient_zero_at_origin line 4253
lemma OAI.UniformMoment.centered_normalization_bounds line 4260
def OAI.C11Compactness.normalizedLipschitz line 4306
lemma OAI.C11Compactness.normalizedLipschitz_pointwise line 4310
lemma OAI.C11Compactness.normalizedLipschitz_compact line 4320
lemma OAI.C11Compactness.normalizedLipschitz_subsequence line 4338
lemma OAI.C11Compactness.pointwise_cauchy_of_gradient line 4354
lemma OAI.C11Compactness.subsequence line 4371
def OAI.MomentLimits.density line 4415
def OAI.MomentLimits.source line 4416
lemma OAI.MomentLimits.continuous_density line 4420
lemma OAI.MomentLimits.integral_source line 4423
lemma OAI.MomentLimits.source_finite line 4431
lemma OAI.MomentLimits.integral_density_tendsto line 4434
lemma OAI.MomentLimits.density_le_limit_bound line 4448
lemma OAI.MomentLimits.density_integrable_limit line 4455
lemma OAI.MomentLimits.density_integral_one line 4465
lemma OAI.MomentLimits.source_probability line 4476
lemma OAI.MomentLimits.integral_composed_tendsto line 4485
theorem OAI.MomentLimits.map_source_limit line 4507
lemma OAI.MomentLimits.normalized_exhaustion line 4539
lemma OAI.GlobalMoment.supporting_plane line 4567
lemma OAI.GlobalMoment.tilted_potential_coercive line 4582
theorem OAI.GlobalMoment.gradient_surjective_of_dense line 4637
lemma OAI.GlobalMoment.denseRange_of_pushforward line 4667
theorem OAI.GlobalMoment.gradient_surjective_of_pushforward line 4678
lemma OAI.CompactMomentVariational.normalizedSource_openPos line 4695
lemma OAI.CompactMomentVariational.integral_truncated_target line 4705
lemma OAI.CompactMomentVariational.truncated_target_tendsto line 4720
theorem OAI.CompactMomentVariational.exists_C11_global line 4742
lemma OAI.CompactMomentVariational.finite_dual_of_surjective_gradient line 4828
lemma OAI.CompactMomentVariational.C1_inverse line 4843
lemma OAI.CompactMomentVariational.C1_weak_MA line 4858
lemma OAI.CompactMomentVariational.convex_gradient_derivative_positive line 4894
theorem OAI.CompactMomentVariational.C11_ae_positive_MA line 4905
lemma OAI.LocalEllipticity.positive_closed line 4967
lemma OAI.LocalEllipticity.positive_inner line 4983
lemma OAI.LocalEllipticity.uniform_coercivity line 5007
theorem OAI.CompactMomentVariational.C11_locally_uniformly_elliptic line 5048
def OAI.MomentLinearization.hessian line 5088
def OAI.MomentLinearization.vectorDiff line 5091
def OAI.MomentLinearization.matrixDiff line 5093
lemma OAI.MomentLinearization.discrete_subsolution line 5096
theorem OAI.MomentLinearization.C11_ae_subsolution line 5125
def OAI.InverseElliptic.fromMatrix line 5154
lemma OAI.InverseElliptic.fromMatrix_toMatrix line 5156
lemma OAI.InverseElliptic.toMatrix_fromMatrix line 5162
lemma OAI.InverseElliptic.inverse_continuousOn line 5167
theorem OAI.InverseElliptic.compact_inverse_bounds line 5174
lemma OAI.MomentLinearization.continuous_gradient_of_C1 line 5229
theorem OAI.MomentLinearization.C11_local_coefficients line 5233
lemma OAI.RadialBarrier.gradient_radial line 5327
lemma OAI.RadialBarrier.hessian_radial line 5338
lemma OAI.RadialBarrier.profile_deriv line 5356
lemma OAI.RadialBarrier.profile_second line 5361
lemma OAI.RadialBarrier.hessian_power line 5368
lemma OAI.RadialBarrier.matrix_rank_one line 5385
lemma OAI.RadialBarrier.trace_hessian_power line 5405
lemma OAI.RadialBarrier.coord_dot_self line 5417
lemma OAI.RadialBarrier.trace_upper line 5422
lemma OAI.RadialBarrier.quadratic_lower line 5429
def OAI.RadialBarrier.profile line 5445
lemma OAI.RadialBarrier.power_shift line 5447
lemma OAI.RadialBarrier.norm_gradient_profile line 5452
lemma OAI.RadialBarrier.trace_lower line 5459
lemma OAI.RadialBarrier.profile_coarse_bound line 5475
lemma OAI.RadialBarrier.profile_positive_annulus line 5505
lemma OAI.SmoothCompactify.gradient_contDiff line 5538
lemma OAI.SmoothCompactify.gradient_hasCompactSupport line 5542
lemma OAI.SmoothCompactify.gradient_lipschitz line 5546
theorem OAI.SmoothCompactify.exists_extension line 5556
lemma OAI.RadialBarrier.profile_contDiff line 5581
lemma OAI.RadialBarrier.gradient_affine line 5584
lemma OAI.RadialBarrier.hessian_affine line 5592
lemma OAI.RadialBarrier.trace_affine line 5598
theorem OAI.RadialBarrier.exists_elliptic_barrier line 5607
lemma OAI.ABPGeometry.second_nonpos_at_localMax line 5710
lemma OAI.ABPGeometry.localMax_hessian_nonpos line 5737
def OAI.ABPGeometry.upperContact line 5759
lemma OAI.ABPGeometry.upperContact_measurable line 5762
lemma OAI.ABPGeometry.small_slope_in_contact_image line 5771
lemma OAI.ABPGeometry.gradient_sub_inner line 5805
lemma OAI.ABPGeometry.hessian_isSymmetric line 5814
lemma OAI.ABPGeometry.contact_hessian_negative line 5823
lemma OAI.ABPGeometry.small_slope_in_positive_contact_image line 5848
lemma OAI.ABPGeometry.lipschitz_image_null line 5867
lemma OAI.ABPGeometry.lipschitz_area_upper_bound line 5876
lemma OAI.ABPGeometry.positive_height_measure_bound line 5896
lemma OAI.ABPMatrix.trace_mul_nonneg line 5917
lemma OAI.ABPMatrix.det_le_trace_pow line 5925
lemma OAI.ABPMatrix.det_le_of_trace line 5937
def OAI.ABPGeometry.hessianMatrix line 5956
lemma OAI.ABPGeometry.contact_det_bound line 5960
theorem OAI.ABPGeometry.abp_contact_estimate line 5979
theorem OAI.ABPGeometry.abp_contact_mass line 5999
def OAI.ABPGeometry.boundedContact line 6014
lemma OAI.ABPGeometry.boundedContact_measurable line 6017
lemma OAI.ABPGeometry.bounded_slopes_image line 6024
theorem OAI.ABPGeometry.abp_bounded_slopes line 6034
theorem OAI.ABPGeometry.abp_localized_contact_mass line 6051
lemma OAI.ABPGeometry.gradient_sub_of_diff line 6075
lemma OAI.ABPGeometry.hessian_sub_of_diff line 6083
theorem OAI.ABPGeometry.barrier_contact_mass line 6092
theorem OAI.HarnackOneStep.exists_mass_constants line 6148
def OAI.DyadicBoxes.box line 6196
lemma OAI.DyadicBoxes.box_le line 6201
lemma OAI.DyadicBoxes.comparable line 6207
lemma OAI.DyadicBoxes.same_level_disjoint line 6221
lemma OAI.DyadicBoxes.level_cover line 6238
lemma OAI.DyadicBoxes.side_length line 6248
lemma OAI.DyadicBoxes.box_append line 6256
lemma OAI.DyadicBoxes.diameter_bound line 6261
lemma OAI.DyadicBoxes.exists_small_level line 6267
def OAI.CubeGeometry.unitBox line 6289
def OAI.CubeGeometry.center line 6290
def OAI.CubeGeometry.side line 6291
lemma OAI.CubeGeometry.side_pos line 6294
lemma OAI.CubeGeometry.side_le_one line 6296
lemma OAI.CubeGeometry.sides line 6300
lemma OAI.CubeGeometry.norm_le_card_mul line 6305
lemma OAI.CubeGeometry.center_mem line 6320
lemma OAI.CubeGeometry.norm_center line 6326
lemma OAI.CubeGeometry.preimage_box line 6342
lemma OAI.CubeGeometry.inner_ball_subset line 6361
lemma OAI.CubeGeometry.volume_unitBox line 6367
lemma OAI.CubeGeometry.volume_unitCube line 6372
lemma OAI.CubeGeometry.parent_side line 6379
lemma OAI.CubeGeometry.normalized_parent line 6383
lemma OAI.CubeGeometry.global_ball line 6407
lemma OAI.CubeGeometry.norm_unit line 6420
lemma OAI.MassDecay.of_positive_mass line 6434
lemma OAI.MassDecay.constants line 6455
theorem OAI.HarnackCube.exists_decay line 6471
lemma OAI.AffineMeasure.quasi line 6516
lemma OAI.AffineMeasure.affine_image line 6519
lemma OAI.AffineMeasure.preimage line 6529
lemma OAI.AffineRescale.hasFDerivAt_map line 6549
lemma OAI.AffineRescale.differentiable line 6554
lemma OAI.AffineRescale.gradient line 6558
lemma OAI.AffineRescale.hessian line 6570
lemma OAI.AffineRescale.gradient_lipschitz line 6586
lemma OAI.HarnackScale.pde_rescale line 6610
def OAI.LaminarCover.maximal line 6643
lemma OAI.LaminarCover.covered_by_maximal line 6647
lemma OAI.LaminarCover.maximal_disjoint line 6666
theorem OAI.LaminarCover.measure_le_of_laminar_cover line 6675
lemma OAI.DyadicBoxes.good_parents_cover line 6711
theorem OAI.DyadicBoxes.ink_spots line 6753
theorem OAI.DyadicBoxes.superlevel_tail line 6778
lemma OAI.WeakHarnack.toLp_measure line 6824
lemma OAI.WeakHarnack.toLp_box_measure line 6832
lemma OAI.WeakHarnack.box_pos line 6837
lemma OAI.WeakHarnack.rescale_density line 6845
theorem OAI.WeakHarnack.exists_tail line 6866
lemma OAI.TailLimit.superlevel line 6947
lemma OAI.TailLimit.finite_common line 6966
theorem OAI.WeakHarnack.exists_limit_tail line 6989
def OAI.SecondDifference.scalar line 7019
def OAI.SecondDifference.vector line 7021
lemma OAI.SecondDifference.scalar_hasFDerivAt line 7024
lemma OAI.SecondDifference.gradient_scalar line 7035
lemma OAI.SecondDifference.vector_hasFDerivAt line 7042
lemma OAI.SecondDifference.matrix_gradient_scalar line 7053
def OAI.DeficitQuotient.hessian line 7076
def OAI.DeficitQuotient.deficit line 7079
lemma OAI.DeficitQuotient.differentiable line 7083
lemma OAI.DeficitQuotient.gradient_deficit line 7088
lemma OAI.DeficitQuotient.gradient_lipschitz line 7098
lemma OAI.DeficitQuotient.hessian_deficit line 7123
lemma OAI.DeficitQuotient.pde line 7140
lemma OAI.AESlice.ae_lines line 7170
lemma OAI.AESlice.line_lipschitz line 7186
lemma OAI.AESlice.line_deriv line 7193
lemma OAI.AESlice.difference_le_ae line 7197
lemma OAI.AESlice.second_difference_le line 7245
lemma OAI.SecondQuotient.scalar_limit line 7302
lemma OAI.SecondQuotient.gradient_limit line 7329
lemma OAI.C11Difference.directional_bound line 7357
lemma OAI.C11Difference.scalar_bound line 7365
lemma OAI.C11Difference.deficit_limit line 7374
theorem OAI.HessianTail.exists_constants line 7397
lemma OAI.SmallSequence.exists_shift_sequence line 7466
def OAI.OscillationEnvelope.upper line 7501
def OAI.OscillationEnvelope.lower line 7502
def OAI.OscillationEnvelope.span line 7503
lemma OAI.OscillationEnvelope.le_upper line 7506
lemma OAI.OscillationEnvelope.lower_le line 7507
lemma OAI.OscillationEnvelope.upper_mono line 7508
lemma OAI.OscillationEnvelope.lower_mono line 7510
lemma OAI.OscillationEnvelope.span_nonneg line 7512
lemma OAI.OscillationEnvelope.exists_near_upper line 7516
lemma OAI.OscillationEnvelope.span_le_of_osc line 7522
lemma OAI.OscillationEnvelope.span_drop line 7534
lemma OAI.OscillationEnvelope.sum_drop line 7542
def OAI.HessianTail.cube line 7561
def OAI.HessianTail.direction line 7562
lemma OAI.HessianTail.direction_bound line 7565
lemma OAI.HessianTail.direction_bddAbove line 7573
lemma OAI.HessianTail.direction_bddBelow line 7580
lemma OAI.HessianTail.cube_measure_inter line 7587
lemma OAI.HessianTail.small_ball_nonempty line 7595
theorem OAI.HessianTail.exists_envelope_constants line 7599
def OAI.FiniteElliptic.quadratic line 7667
lemma OAI.FiniteElliptic.quadratic_continuous line 7670
lemma OAI.FiniteElliptic.quadratic_smul line 7675
lemma OAI.FiniteElliptic.hermitian_closed line 7680
lemma OAI.FiniteElliptic.positive_closed line 7684
lemma OAI.FiniteElliptic.trace_mul_nonneg line 7692
lemma OAI.FiniteElliptic.trace_mul_pos line 7700
theorem OAI.FiniteElliptic.exists_directions line 7709
lemma OAI.EllipticOscillation.quadratic_sub line 7808
lemma OAI.EllipticOscillation.abs_quadratic_le line 7813
theorem OAI.EllipticOscillation.high_point_control line 7834
lemma OAI.EllipticOscillation.contraction line 7865
lemma OAI.FiniteOscillation.sum_span_of_high_point line 7884
theorem OAI.FiniteOscillation.exists_contraction line 7903
def OAI.HessianCoordinates.vector line 7987
lemma OAI.HessianCoordinates.quadratic_toMatrix line 7989
def OAI.InteriorOscillation.oscillation line 8012
theorem OAI.InteriorOscillation.exists_constants line 8015
def OAI.MARescale.potential line 8090
def OAI.MARescale.point line 8092
lemma OAI.MARescale.point_add line 8095
lemma OAI.MARescale.point_sub line 8098
lemma OAI.MARescale.scalar line 8102
lemma OAI.MARescale.gradient line 8111
lemma OAI.MARescale.gradient_lipschitz line 8117
lemma OAI.MARescale.hessian line 8131
lemma OAI.MARescale.vector line 8140
lemma OAI.MARescale.pde line 8147
lemma OAI.OscillationScale.dist_point line 8171
lemma OAI.OscillationScale.image_ball line 8175
lemma OAI.OscillationScale.span_comp line 8192
lemma OAI.OscillationScale.span_congr line 8198
lemma OAI.MARescale.differentiable_potential line 8213
lemma OAI.MARescale.differentiable_gradient line 8217
theorem OAI.InteriorOscillation.exists_scaled_constants line 8236
theorem OAI.OscillationIteration.exists_bound line 8329
theorem OAI.OscillationIteration.tendsto_zero line 8360
def OAI.OscillationDecay.total line 8376
lemma OAI.OscillationDecay.total_nonneg line 8379
lemma OAI.OscillationDecay.difference_le_total line 8384
lemma OAI.OscillationDecay.ball_inter_nonempty line 8392
theorem OAI.OscillationDecay.vanishing_at line 8397
theorem OAI.MatrixOscillation.vanishing_at line 8443
theorem OAI.ContinuousEnvelope.exists_continuous_extension line 8489
theorem OAI.C11InteriorRegularity.continuous_hessian_rep line 8530
lemma OAI.AEContinuousDerivative.increment_bound line 8614
theorem OAI.AEContinuousDerivative.hasFDerivAt_of_ae line 8648
theorem OAI.AEContinuousDerivative.contDiff_one_of_matrix_rep line 8672
lemma OAI.AEContinuousDerivative.contDiff_two_of_gradient line 8698
theorem OAI.CompactMomentVariational.C11_to_C2 line 8715
theorem OAI.CompactMomentVariational.C2_positive_MA line 8742
lemma OAI.MomentLinearization.continuous_gradient_of_C1_pair line 8798
theorem OAI.MomentLinearization.C11_local_coefficients_pair line 8802
theorem OAI.OscillationDecay.exists_grid_constants line 8888
lemma OAI.GridHolder.exponent line 8936
lemma OAI.GridHolder.pow_rpow line 8949
theorem OAI.GridHolder.of_grid line 8953
theorem OAI.C11InteriorRegularity.holder_hessian line 8983
theorem OAI.CompactMomentVariational.C2_local_holder line 9125
lemma OAI.LocalPeetre.rpow_compare line 9167
def OAI.LocalPeetre.weight line 9189
lemma OAI.LocalPeetre.quadratic_add line 9191
lemma OAI.LocalPeetre.weight_pos line 9198
theorem OAI.LocalPeetre.weight_sub line 9202
lemma OAI.LocalConvolution.integral_mul_le_L2 line 9223
lemma OAI.LocalConvolution.integral_sq_eq_norm_sq line 9233
theorem OAI.LocalConvolution.norm_le_convolution_majorant line 9243
lemma OAI.LocalFourier.fourierInv_pairing line 9308
lemma OAI.LocalFourier.fourierInv_apply line 9314
lemma OAI.LocalFourier.fourier_pairing_apply line 9316
abbrev OAI.SobolevModel.Model line 9343
def OAI.SobolevModel.embedding line 9347
lemma OAI.SobolevModel.embedding_injective line 9350
lemma OAI.SobolevModel.embedding_memSobolev line 9358
lemma OAI.SobolevModel.memSobolev_iff_range line 9363
def OAI.SobolevModel.schwartzBessel line 9375
lemma OAI.SobolevModel.schwartzBessel_add line 9379
lemma OAI.SobolevModel.schwartzBessel_zero line 9390
lemma OAI.SobolevModel.schwartzBessel_surjective line 9393
def OAI.SobolevModel.coordinate line 9398
lemma OAI.SobolevModel.schwartzBessel_distribution line 9401
lemma OAI.SobolevModel.embedding_coordinate line 9406
lemma OAI.SobolevModel.denseRange_coordinate line 9414
theorem OAI.SobolevModel.lift_operator line 9419
lemma OAI.LocalSobolev.weight_growth line 9452
def OAI.LocalSobolev.weighted line 9456
lemma OAI.LocalSobolev.weighted_apply line 9460
lemma OAI.LocalSobolev.norm_weighted line 9465
lemma OAI.LocalSobolev.norm_coordinate line 9469
lemma OAI.LocalSobolev.integrable_norm_product line 9479
lemma OAI.LocalSobolev.weighted_fourier_majorant line 9485
lemma OAI.LocalSobolev.toLp_norm_norm line 9514
theorem OAI.LocalSobolev.multiplication_bound line 9518
lemma OAI.LocalSobolev.multiplication_distribution line 9537
theorem OAI.LocalSobolev.multiplication_lift line 9550
lemma OAI.LocalSobolev.continuous_multiplier_gauge line 9560
lemma OAI.LocalSobolev.weight_add line 9574
lemma OAI.LocalSobolev.fourier_multiplier_bound line 9578
theorem OAI.LocalSobolev.fourier_multiplier_lift line 9595
lemma OAI.SobolevModel.kernel_eq_zero_of_small line 9612
theorem OAI.SobolevModel.regularity_of_small_perturbation line 9626
def OAI.LocalParametrix.coefficientGauge line 9659
lemma OAI.LocalParametrix.coefficientGauge_nonneg line 9662
lemma OAI.LocalParametrix.coefficientGauge_zero line 9666
lemma OAI.LocalParametrix.continuous_coefficientGauge line 9671
def OAI.LocalParametrix.perturbation line 9674
theorem OAI.LocalParametrix.perturbation_lift line 9680
theorem OAI.LocalParametrix.gain_of_small_principal line 9720
theorem OAI.LocalParametrix.eventually_small_coefficients line 9734
def OAI.LocalDifferential.product line 9762
lemma OAI.LocalDifferential.product_apply line 9764
lemma OAI.LocalDifferential.schwartz_product_derivative line 9767
lemma OAI.LocalDifferential.product_neg_right line 9776
theorem OAI.LocalDifferential.derivative_multiply line 9779
def OAI.LocalDifferential.derivative line 9791
theorem OAI.LocalDifferential.derivative_nil line 9795
theorem OAI.LocalDifferential.derivative_cons line 9796
theorem OAI.LocalDifferential.derivative_sobolev line 9802
theorem OAI.LocalBootstrap.multiply_sobolev line 9819
theorem OAI.LocalBootstrap.commutator_sobolev line 9826
lemma OAI.LocalBootstrap.sobolev_finset_sum line 9857
theorem OAI.LocalBootstrap.lower_order_sobolev line 9867
theorem OAI.LocalBootstrap.gain_from_frozen_equation line 9878
def OAI.LocalDifferential.symbol line 9922
def OAI.LocalDifferential.symbolConstant line 9926
lemma OAI.LocalDifferential.symbolConstant_nonneg line 9931
lemma OAI.LocalDifferential.symbol_growth line 9936
lemma OAI.LocalDifferential.norm_le_weight_one line 9943
lemma OAI.LocalDifferential.symbol_bound line 9948
lemma OAI.LocalDifferential.weighted_symbol_bound line 9967
lemma OAI.LocalDifferential.derivative_fourier line 9979
def OAI.LocalSupport.SupportedIn line 10000
lemma OAI.LocalSupport.supported_multiply line 10003
lemma OAI.LocalSupport.SupportedIn.lineDeriv line 10016
lemma OAI.LocalSupport.SupportedIn.derivative line 10027
lemma OAI.LocalSupport.SupportedIn.multiply_congr line 10033
lemma OAI.LocalSupport.SupportedIn.cutoff_identity line 10046
def OAI.LocalOperator.operator line 10060
lemma OAI.LocalOperator.operator_apply line 10063
lemma OAI.LocalOperator.multiply_comm line 10067
lemma OAI.LocalOperator.operator_cutoff line 10072
def OAI.LocalOperator.perturbCoefficient line 10084
lemma OAI.LocalOperator.perturb_on_cutoff line 10088
def OAI.LocalOperator.frozenSymbol line 10104
lemma OAI.LocalOperator.frozenSymbol_growth line 10108
lemma OAI.LocalOperator.fourier_add line 10116
lemma OAI.LocalOperator.sumSymbol_growth line 10122
lemma OAI.LocalOperator.sumSymbol_operator line 10129
lemma OAI.LocalOperator.frozenSymbol_operator line 10141
lemma OAI.LocalOperator.frozen_equation line 10148
theorem OAI.LocalOperator.gain_for_localized_operator line 10161
lemma OAI.LocalSchwartz.contDiff_partial_iterated line 10214
lemma OAI.LocalSchwartz.tendsto_zero_of_compact_support line 10231
def OAI.LocalSchwartz.frozenDifference line 10261
theorem OAI.LocalSchwartz.frozenDifference_tendsto line 10266
def OAI.LocalOperator.frozenCoefficient line 10289
lemma OAI.LocalOperator.frozenCoefficient_apply line 10294
lemma OAI.LocalOperator.perturb_frozen_tendsto line 10301
theorem OAI.LocalOperator.frozen_coefficients_eventually_small line 10313
theorem OAI.LocalOperator.eventually_gain_rescaled line 10326
def OAI.AffineDistribution.homothety line 10352
lemma OAI.AffineDistribution.homothety_apply line 10355
def OAI.AffineDistribution.translate line 10358
lemma OAI.AffineDistribution.translate_apply line 10361
def OAI.AffineDistribution.jac line 10364
def OAI.AffineDistribution.dilate line 10366
lemma OAI.AffineDistribution.dilate_apply line 10371
lemma OAI.AffineDistribution.homothety_symm_apply line 10375
lemma OAI.AffineDistribution.dilate_lineDeriv line 10378
lemma OAI.AffineDistribution.dilate_multiply line 10385
lemma OAI.AffineDistribution.memLp_dilate line 10400
lemma OAI.AffineDistribution.dilate_Lp line 10407
lemma OAI.AffineDistribution.fourier_comp_dilate line 10427
lemma OAI.AffineDistribution.fourier_schwartz_dilate line 10434
lemma OAI.AffineDistribution.fourier_dilate_test line 10444
lemma OAI.AffineDistribution.jac_inv line 10450
lemma OAI.AffineDistribution.jac_ne_zero line 10454
lemma OAI.AffineDistribution.fourier_dilate line 10458
def OAI.AffineDistribution.scaleWeight line 10470
lemma OAI.AffineDistribution.scaleWeight_growth line 10474
lemma OAI.AffineDistribution.scaleWeight_bounded line 10481
lemma OAI.AffineDistribution.scaleWeight_mul line 10515
lemma OAI.AffineDistribution.rescaled_fourier_Lp line 10524
theorem OAI.AffineDistribution.memSobolev_dilate line 10546
lemma OAI.AffineDistribution.test_translate_lineDeriv line 10574
lemma OAI.AffineDistribution.translate_lineDeriv line 10589
lemma OAI.AffineDistribution.translate_derivative line 10595
lemma OAI.AffineDistribution.dilate_derivative line 10601
lemma OAI.AffineDistribution.translate_multiply line 10613
lemma OAI.AffineDistribution.translate_translate line 10624
lemma OAI.AffineDistribution.translate_zero line 10632
lemma OAI.AffineDistribution.dilate_inv_dilate line 10639
lemma OAI.AffineDistribution.dilate_derivative_inverse line 10648
def OAI.TranslationSobolev.translate line 10663
lemma OAI.TranslationSobolev.translate_schwartz line 10667
lemma OAI.TranslationSobolev.norm_fourier_translate line 10676
def OAI.TranslationSobolev.weighted line 10685
lemma OAI.TranslationSobolev.norm_coordinate line 10688
lemma OAI.TranslationSobolev.norm_coordinate_translate_le line 10697
theorem OAI.TranslationSobolev.memSobolev_translate line 10714
def OAI.AffineDistribution.transform line 10732
lemma OAI.AffineDistribution.transform_multiply line 10735
lemma OAI.AffineDistribution.transform_derivative line 10744
def OAI.AffineDistribution.physicalCutoff line 10751
lemma OAI.AffineDistribution.physicalCutoff_apply line 10755
lemma OAI.AffineDistribution.transform_cutoff line 10758
lemma OAI.AffineDistribution.inverse_transform line 10766
lemma OAI.AffineDistribution.memSobolev_transform line 10773
lemma OAI.AffineDistribution.memSobolev_of_transform line 10778
lemma OAI.AffineDistribution.memSobolev_physicalCutoff line 10785
lemma OAI.AffineDistribution.frozen_cutoff line 10798
lemma OAI.AffineDistribution.power_normalize line 10812
lemma OAI.AffineDistribution.transform_term line 10818
lemma OAI.AffineDistribution.normalized_term line 10828
lemma OAI.AffineDistribution.normalized_operator line 10842
lemma OAI.AffineDistribution.normalized_weak_equation line 10860
theorem OAI.AffineDistribution.eventually_physical_gain line 10876
lemma OAI.LocalSupport.supported_multiply_growth line 10904
lemma OAI.LocalSupport.SupportedIn.annihilate line 10917
lemma OAI.LocalSupport.cutoff_derivative_eq line 10927
def OAI.SobolevGerms.At line 10962
def OAI.SobolevGerms.aggregate line 10965
lemma OAI.SobolevGerms.aggregate_eq_one line 10970
lemma OAI.SobolevGerms.aggregate_sobolev line 10980
theorem OAI.SobolevGerms.compact_cutoff line 11001
def OAI.LocalBumps.complexBump line 11043
lemma OAI.LocalBumps.complexBump_apply line 11047
lemma OAI.LocalBumps.complexBump_tsupport line 11050
lemma OAI.LocalBumps.complexBump_compact line 11055
lemma OAI.LocalBumps.complexBump_one line 11059
def OAI.LocalBumps.innerBump line 11064
def OAI.LocalBumps.outerBump line 11065
def OAI.LocalBumps.inner line 11067
def OAI.LocalBumps.outer line 11068
lemma OAI.LocalBumps.inner_compact line 11070
lemma OAI.LocalBumps.outer_compact line 11071
lemma OAI.LocalBumps.inner_tsupport line 11072
lemma OAI.LocalBumps.inner_one line 11073
lemma OAI.LocalBumps.outer_covers_inner line 11075
lemma OAI.AffineDistribution.physicalCutoff_one line 11092
lemma OAI.AffineDistribution.physical_inner_bound line 11100
lemma OAI.AffineDistribution.eventually_physical_covered line 11116
lemma OAI.LocalSupport.cutoff_operator_eq line 11137
lemma OAI.LocalSupport.cutoff_multiply_eq line 11148
lemma OAI.LocalSupport.cutoff_zero line 11154
theorem OAI.LocalElliptic.gain_at line 11170
theorem OAI.SobolevGerms.compact_cutoff_on line 11214
lemma OAI.SobolevSmooth.weighted_L1_of_distribution_eq line 11259
theorem OAI.SobolevSmooth.exists_fourier_all_moments line 11279
theorem OAI.SobolevSmooth.exists_smooth_fourier_representative line 11307
theorem OAI.SobolevSmooth.smooth_representative line 11314
theorem OAI.LocalElliptic.all_orders_at line 11352
lemma OAI.LocalElliptic.at_of_memSobolev line 11370
lemma OAI.LocalElliptic.physical_inner_compact line 11377
theorem OAI.LocalElliptic.local_smooth_cutoffs line 11383
lemma OAI.SmoothPatching.cutoff_rep_ae line 11401
theorem OAI.SmoothPatching.patch line 11418
theorem OAI.LocalElliptic.smooth_of_elliptic_Lp line 11475
abbrev OAI.DistributionExpansion.Term line 11504
def OAI.DistributionExpansion.evalTerm line 11506
def OAI.DistributionExpansion.eval line 11509
lemma OAI.DistributionExpansion.eval_nil line 11512
lemma OAI.DistributionExpansion.eval_cons line 11513
lemma OAI.DistributionExpansion.derivative_add line 11516
def OAI.DistributionExpansion.differentiate line 11520
lemma OAI.DistributionExpansion.eval_differentiate line 11523
lemma OAI.DistributionExpansion.differentiate_order line 11535
def OAI.DistributionExpansion.lower line 11545
lemma OAI.DistributionExpansion.derivative_multiply_expansion line 11549
lemma OAI.DistributionExpansion.lower_order line 11561
lemma OAI.DistributionExpansion.eval_append line 11584
lemma OAI.DistributionExpansion.eval_flatten line 11588
lemma OAI.DistributionExpansion.eval_ofFn line 11596
lemma OAI.DistributionExpansion.eval_eq_sum line 11600
lemma OAI.DistributionExpansion.eval_flatten_ofFn line 11604
def OAI.DistributionExpansion.divergence line 11609
def OAI.DistributionExpansion.lowerTerms line 11612
lemma OAI.DistributionExpansion.divergence_expansion line 11617
lemma OAI.DistributionExpansion.lowerTerms_order line 11625
theorem OAI.DistributionExpansion.smooth_of_divergence_Lp line 11646
def OAI.DistributionExpansion.testDerivative line 11684
lemma OAI.DistributionExpansion.derivative_pairing line 11688
def OAI.DistributionExpansion.testOperator line 11699
lemma OAI.DistributionExpansion.divergence_pairing line 11703
lemma OAI.DistributionExpansion.localized_vanishes line 11710
lemma OAI.DistributionExpansion.localized_vanishes_Lp line 11723
abbrev OAI.SchwartzOperator.Term line 11743
def OAI.SchwartzOperator.derivative line 11745
lemma OAI.SchwartzOperator.derivative_nil line 11749
lemma OAI.SchwartzOperator.derivative_cons line 11750
lemma OAI.SchwartzOperator.derivative_append line 11753
def OAI.SchwartzOperator.term line 11759
def OAI.SchwartzOperator.operator line 11762
lemma OAI.SchwartzOperator.term_apply line 11764
lemma OAI.SchwartzOperator.operator_nil line 11766
lemma OAI.SchwartzOperator.operator_cons line 11767
lemma OAI.SchwartzOperator.operator_append line 11770
lemma OAI.SchwartzOperator.operator_map_coefficient line 11774
def OAI.SchwartzOperator.differentiate line 11784
lemma OAI.SchwartzOperator.operator_differentiate line 11787
def OAI.SchwartzOperator.lower line 11799
lemma OAI.SchwartzOperator.derivative_product line 11803
lemma OAI.SchwartzOperator.lower_order line 11813
lemma OAI.SchwartzOperator.operator_append_directions line 11828
def OAI.SchwartzOperator.composeLower line 11834
def OAI.SchwartzOperator.composeTerm line 11837
lemma OAI.SchwartzOperator.operator_composeTerm line 11840
lemma OAI.SchwartzOperator.composeLower_order line 11852
lemma OAI.SchwartzOperator.composeTerm_order line 11859
def OAI.SchwartzOperator.compose line 11867
def OAI.SchwartzOperator.principalCompose line 11870
def OAI.SchwartzOperator.lowerCompose line 11873
lemma OAI.SchwartzOperator.operator_compose_fixed line 11876
lemma OAI.SchwartzOperator.operator_compose line 11883
lemma OAI.SchwartzOperator.operator_compose_split_fixed line 11891
lemma OAI.SchwartzOperator.operator_compose_split line 11901
lemma OAI.SchwartzOperator.principalCompose_order line 11913
lemma OAI.SchwartzOperator.lowerCompose_order line 11922
lemma OAI.SchwartzOperator.compose_order line 11931
def OAI.SchwartzOperator.negTerms line 11940
lemma OAI.SchwartzOperator.operator_negTerms line 11942
def OAI.SchwartzOperator.secondOrderRemainder line 11953
lemma OAI.SchwartzOperator.secondOrder_square_expansion line 11956
lemma OAI.SchwartzOperator.secondOrderRemainder_order line 11966
lemma OAI.SchwartzOperator.testDerivative_append line 11988
lemma OAI.SchwartzOperator.testDerivative_reverse line 11997
def OAI.SchwartzOperator.adjointTerm line 12005
lemma OAI.SchwartzOperator.adjointTerm_pairing line 12009
def OAI.SchwartzOperator.adjoint line 12021
lemma OAI.SchwartzOperator.adjoint_pairing line 12024
lemma OAI.SchwartzOperator.adjoint_ofFn line 12032
lemma OAI.SchwartzOperator.adjoint_eq_divergence line 12038
lemma OAI.SchwartzOperator.localized_adjoint_vanishes line 12044
lemma OAI.LocalSymbol.rpow_growth line 12071
def OAI.LocalSymbol.quadratic line 12140
def OAI.LocalSymbol.principal line 12141
def OAI.LocalSymbol.regularized line 12142
def OAI.LocalSymbol.inverseSymbol line 12143
lemma OAI.LocalSymbol.quadratic_growth line 12146
lemma OAI.LocalSymbol.principal_growth line 12150
lemma OAI.LocalSymbol.regularized_growth line 12153
lemma OAI.LocalSymbol.inverseSymbol_growth line 12156
lemma OAI.LocalSymbol.inverse_identity line 12164
lemma OAI.LocalSymbol.inverse_order_bound line 12172
lemma OAI.LocalSymbol.exists_coercivity line 12198
lemma OAI.FourthOrderSymbol.symbol_append line 12230
lemma OAI.FourthOrderSymbol.symbol_pair line 12236
lemma OAI.FourthOrderSymbol.quadratic_expansion line 12246
lemma OAI.FourthOrderSymbol.second_symbol line 12264
lemma OAI.FourthOrderSymbol.fourth_symbol line 12278
lemma OAI.SchwartzOperator.symbol_reverse line 12317
def OAI.SchwartzOperator.testSymbol line 12326
lemma OAI.SchwartzOperator.testSymbol_nil line 12329
lemma OAI.SchwartzOperator.testSymbol_cons line 12330
lemma OAI.SchwartzOperator.testSymbol_append line 12332
lemma OAI.SchwartzOperator.testSymbol_principal_fixed line 12336
lemma OAI.SchwartzOperator.testSymbol_principalCompose line 12345
lemma OAI.SchwartzOperator.testSymbol_ofFn line 12353
lemma OAI.SchwartzOperator.testSymbol_eq_sum line 12357
theorem OAI.SchwartzOperator.smooth_of_weak_square line 12369
structure OAI.SmoothOperator.Coefficient line 12446
instance OAI.SmoothOperator.(instance at line 12450) line 12450
abbrev OAI.SmoothOperator.Term line 12451
def OAI.SmoothOperator.derivative line 12453
lemma OAI.SmoothOperator.derivative_smooth line 12457
lemma OAI.SmoothOperator.derivative_eq_schwartz line 12463
lemma OAI.SmoothOperator.derivative_support line 12471
lemma OAI.SmoothOperator.derivative_compact line 12483
def OAI.SmoothOperator.operator line 12487
lemma OAI.SmoothOperator.operator_nil line 12490
lemma OAI.SmoothOperator.operator_cons line 12491
lemma OAI.SmoothOperator.operator_append line 12494
lemma OAI.SmoothOperator.operator_smooth line 12497
lemma OAI.SmoothOperator.operator_support line 12503
lemma OAI.SmoothOperator.operator_compact line 12512
def OAI.SmoothOperator.localizeTerm line 12516
def OAI.SmoothOperator.localize line 12519
lemma OAI.SmoothOperator.localize_apply line 12522
lemma OAI.SmoothOperator.localize_operator line 12525
lemma OAI.SmoothOperator.localize_operator_eq line 12539
lemma OAI.SmoothOperator.localize_append line 12552
lemma OAI.SmoothOperator.localize_square line 12555
def OAI.SmoothOperator.testSymbol line 12579
lemma OAI.SmoothOperator.localize_symbol line 12583
lemma OAI.SmoothOperator.localize_order line 12595
lemma OAI.SmoothOperator.localize_order_le line 12603
lemma OAI.SmoothOperator.local_cutoff_pair line 12612
theorem OAI.SmoothOperator.smooth_of_compact_weak_square line 12643
structure OAI.RealSmoothOperator.Coefficient line 12683
instance OAI.RealSmoothOperator.(instance at line 12686) line 12686
abbrev OAI.RealSmoothOperator.Term line 12687
def OAI.RealSmoothOperator.derivative line 12689
lemma OAI.RealSmoothOperator.derivative_smooth line 12693
lemma OAI.RealSmoothOperator.derivative_compact line 12699
def OAI.RealSmoothOperator.operator line 12705
lemma OAI.RealSmoothOperator.operator_smooth line 12708
lemma OAI.RealSmoothOperator.operator_compact line 12714
def OAI.RealSmoothOperator.complexifyTerm line 12724
def OAI.RealSmoothOperator.complexify line 12726
lemma OAI.RealSmoothOperator.derivative_re line 12728
lemma OAI.RealSmoothOperator.derivative_im line 12741
lemma OAI.RealSmoothOperator.operator_re line 12754
lemma OAI.RealSmoothOperator.operator_im line 12767
lemma OAI.RealSmoothOperator.square_re line 12780
lemma OAI.RealSmoothOperator.square_im line 12791
lemma OAI.RealSmoothOperator.complex_weak_square line 12804
lemma OAI.RealSmoothOperator.complexify_append line 12842
theorem OAI.RealSmoothOperator.smooth_of_weak_square line 12845
def OAI.RealSmoothOperator.pushTerm line 12886
def OAI.RealSmoothOperator.push line 12888
lemma OAI.RealSmoothOperator.derivative_push line 12890
lemma OAI.RealSmoothOperator.operator_push line 12903
lemma OAI.RealSmoothOperator.square_push line 12915
lemma OAI.RealSmoothOperator.square_pull line 12923
lemma OAI.RealSmoothOperator.push_append line 12937
abbrev OAI.MatrixOperator.Space line 12945
abbrev OAI.MatrixOperator.Euclid line 12946
def OAI.MatrixOperator.e line 12947
def OAI.MatrixOperator.A line 12948
def OAI.MatrixOperator.principal line 12952
def OAI.MatrixOperator.drift line 12956
lemma OAI.MatrixOperator.principal_length line 12959
lemma OAI.MatrixOperator.drift_length line 12965
lemma OAI.MatrixOperator.operator_actual line 12970
def OAI.MatrixOperator.coordinates line 12979
lemma OAI.MatrixOperator.principal_push_length line 12982
lemma OAI.MatrixOperator.drift_push_length line 12989
lemma OAI.MatrixOperator.inner_coordinates_e line 12995
lemma OAI.MatrixOperator.symbol_two line 13000
lemma OAI.MatrixOperator.principal_symbol line 13009
def OAI.MatrixOperator.frozen line 13027
lemma OAI.MatrixOperator.quadratic_frozen line 13030
lemma OAI.MatrixOperator.principal_elliptic line 13037
lemma OAI.MatrixOperator.weak_coordinate_square line 13056
theorem OAI.MatrixOperator.smooth_of_weak_square line 13087
def OAI.WeightedRegularity.densityMeasure line 13110
lemma OAI.WeightedRegularity.density_absolutelyContinuous line 13113
lemma OAI.WeightedRegularity.integral_density line 13118
lemma OAI.WeightedRegularity.density_mul_memLp line 13127
lemma OAI.WeightedRegularity.weighted_weak line 13146
lemma OAI.WeightedRegularity.smooth_density_quotient line 13156
lemma OAI.WeightedRegularity.integral_reflect line 13166
theorem OAI.MatrixOperator.smooth_of_weighted_weak_square line 13181
def OAI.WeightedCalculus.D line 13208
def OAI.WeightedCalculus.adjoint line 13210
def OAI.WeightedCalculus.weight line 13213
lemma OAI.WeightedCalculus.smooth_D line 13215
lemma OAI.WeightedCalculus.compact_D line 13219
lemma OAI.WeightedCalculus.D_add line 13222
lemma OAI.WeightedCalculus.D_sub line 13227
lemma OAI.WeightedCalculus.D_mul line 13232
lemma OAI.WeightedCalculus.D_comm line 13239
lemma OAI.WeightedCalculus.smooth_adjoint line 13252
lemma OAI.WeightedCalculus.compact_adjoint line 13256
lemma OAI.WeightedCalculus.smooth_weight line 13260
lemma OAI.WeightedCalculus.D_weight line 13263
lemma OAI.WeightedCalculus.commutator line 13271
lemma OAI.WeightedCalculus.D_sum line 13287
lemma OAI.WeightedCalculus.smooth_sum line 13292
lemma OAI.WeightedCalculus.compact_sum line 13296
def OAI.WeightedCalculus.divergence line 13304
lemma OAI.WeightedCalculus.smooth_divergence line 13307
lemma OAI.WeightedCalculus.compact_divergence line 13312
lemma OAI.WeightedCalculus.D_divergence line 13317
def OAI.WeightedCalculus.expectation line 13331
lemma OAI.WeightedCalculus.integrable_weighted line 13334
theorem OAI.WeightedCalculus.integration_by_parts line 13339
lemma OAI.WeightedCalculus.expectation_add line 13378
lemma OAI.WeightedCalculus.expectation_sum line 13386
lemma OAI.WeightedCalculus.divergence_adjoint line 13393
theorem OAI.WeightedCalculus.bochner line 13409
abbrev OAI.MomentCoordinates.Space line 13462
def OAI.MomentCoordinates.basis line 13464
def OAI.MomentCoordinates.pd line 13466
def OAI.MomentCoordinates.grad line 13468
def OAI.MomentCoordinates.hess line 13470
lemma OAI.MomentCoordinates.basis_sum line 13473
lemma OAI.MomentCoordinates.linear_coordinates line 13477
lemma OAI.MomentCoordinates.pd_comp line 13485
lemma OAI.MomentCoordinates.pd_coord line 13498
lemma OAI.MomentCoordinates.smooth_pd line 13504
lemma OAI.MomentCoordinates.smooth_grad line 13507
lemma OAI.MomentCoordinates.pd_comm line 13510
lemma OAI.MomentCoordinates.hess_symm line 13513
lemma OAI.MomentCoordinates.pd_comp_grad line 13516
def OAI.MomentCoordinates.pullA line 13527
def OAI.MomentCoordinates.P line 13531
def OAI.MomentCoordinates.W line 13534
lemma OAI.MomentCoordinates.pd_sum line 13537
lemma OAI.MomentCoordinates.pd_sub line 13541
lemma OAI.MomentCoordinates.pullA_divergence line 13546
lemma OAI.MomentCoordinates.smooth_pullA line 13558
lemma OAI.MomentCoordinates.P_pd line 13563
lemma OAI.MomentCoordinates.smooth_P line 13574
lemma OAI.MomentCoordinates.smooth_W line 13579
theorem OAI.MomentCoordinates.W_gradient line 13583
lemma OAI.MomentCoordinates.W_derivative_symm line 13607
lemma OAI.MomentCoordinates.compact_pulled_pd line 13613
lemma OAI.MomentCoordinates.compact_P line 13619
lemma OAI.MomentCoordinates.compact_W line 13626
lemma OAI.MomentCoordinates.compact_pullA line 13632
theorem OAI.MomentCoordinates.hessian_identity line 13639
def OAI.MomentCoordinates.B line 13679
def OAI.MomentCoordinates.R line 13682
lemma OAI.MomentCoordinates.B_eq_matrix line 13685
lemma OAI.MomentCoordinates.hess_transpose line 13690
lemma OAI.MomentCoordinates.B_symm line 13695
lemma OAI.MomentCoordinates.W_derivative line 13704
lemma OAI.MomentCoordinates.R_symm line 13717
def OAI.MomentDifferential.detMultilinear line 13737
lemma OAI.MomentDifferential.detMultilinear_apply line 13741
lemma OAI.MomentDifferential.smooth_det line 13743
lemma OAI.MomentDifferential.det_updateRow_eq line 13746
lemma OAI.MomentDifferential.det_linearDeriv line 13753
theorem OAI.MomentDifferential.fderiv_det_apply line 13762
lemma OAI.MomentDifferential.smooth_matrix_det line 13768
lemma OAI.MomentDifferential.smooth_adjugate_entry line 13773
lemma OAI.MomentDifferential.smooth_inverse_entry line 13785
def OAI.MomentDifferential.md line 13792
lemma OAI.MomentDifferential.md_mul line 13796
lemma OAI.MomentDifferential.md_const line 13814
theorem OAI.MomentDifferential.md_inverse line 13818
lemma OAI.MomentDifferential.fderiv_matrix_apply line 13834
theorem OAI.MomentDifferential.fderiv_logdet line 13846
lemma OAI.MomentEquation.smooth_hess line 13869
lemma OAI.MomentEquation.pd_add line 13872
lemma OAI.MomentEquation.pd_mul line 13876
def OAI.MomentEquation.C line 13880
lemma OAI.MomentEquation.C_apply line 13883
lemma OAI.MomentEquation.smooth_C line 13886
lemma OAI.MomentEquation.C_symm_last line 13889
lemma OAI.MomentEquation.C_symm_first line 13896
lemma OAI.MomentEquation.pd_trace line 13902
lemma OAI.MomentEquation.pd_logdet line 13909
theorem OAI.MomentEquation.first_moment line 13916
lemma OAI.MomentEquation.smooth_matrix_product line 13933
lemma OAI.MomentEquation.trace_cyclic_four line 13940
theorem OAI.MomentEquation.pd_jacobian_term line 13948
lemma OAI.MomentEquation.pd_hess_gradient line 13964
theorem OAI.MomentEquation.twice_moment_raw line 13986
lemma OAI.MomentEquation.hess_transpose line 14008
lemma OAI.MomentEquation.inverse_transpose line 14013
lemma OAI.MomentEquation.inverse_symm line 14017
lemma OAI.MomentEquation.cubic_div_contract line 14022
theorem OAI.MomentEquation.inverse_divergence line 14035
theorem OAI.MomentEquation.inverse_first_moment line 14051
theorem OAI.MomentEquation.weighted_inverse_divergence line 14072
lemma OAI.MomentEquation.pd_C_swap line 14083
lemma OAI.MomentEquation.trace_fourth line 14091
theorem OAI.MomentEquation.divergence_cubic line 14102
theorem OAI.MomentEquation.twice_moment line 14147
def OAI.TargetCoordinates.target line 14165
lemma OAI.TargetCoordinates.target_pull line 14167
lemma OAI.TargetCoordinates.target_apply line 14174
lemma OAI.TargetCoordinates.smooth_target line 14179
lemma OAI.TargetCoordinates.target_chain line 14183
lemma OAI.TargetCoordinates.pd_target line 14192
lemma OAI.TargetCoordinates.stein line 14204
lemma OAI.TargetCoordinates.divergence_product line 14233
lemma OAI.TargetCoordinates.row_adjoint line 14263
def OAI.TargetCoordinates.sourceMeasure line 14290
def OAI.TargetCoordinates.targetMeasure line 14293
def OAI.TargetCoordinates.normalizedE line 14296
lemma OAI.TargetCoordinates.source_integral line 14302
lemma OAI.TargetCoordinates.target_integral line 14314
lemma OAI.TargetCoordinates.expectation_transport line 14328
lemma OAI.TargetCoordinates.target_expectation line 14336
def OAI.MomentOperator.tau line 14349
def OAI.MomentOperator.A line 14352
def OAI.MomentOperator.flux line 14355
lemma OAI.MomentOperator.A_pull line 14358
lemma OAI.MomentOperator.A_target line 14365
lemma OAI.MomentOperator.smooth_A line 14373
lemma OAI.MomentOperator.compact_A line 14380
lemma OAI.MomentOperator.A_divergence line 14387
lemma OAI.MomentOperator.W_flux line 14412
lemma OAI.MomentOperator.double_divergence line 14433
lemma OAI.MomentOperator.hessian_identity_target line 14444
lemma OAI.MomentMatrix.trace_mul_nonneg line 14485
lemma OAI.MomentMatrix.trace_conjugate_nonneg line 14493
lemma OAI.MomentMatrix.trace_energy_nonneg line 14500
lemma OAI.MomentMatrix.quadratic_cs line 14507
lemma OAI.MomentMatrix.trace_energy_quadratic line 14515
theorem OAI.MomentMatrix.trace_cs line 14532
lemma OAI.MomentMatrix.form_symm line 14543
lemma OAI.MomentMatrix.form_nonneg line 14548
lemma OAI.MomentMatrix.form_quadratic line 14553
lemma OAI.MomentMatrix.integral_quadratic_cs line 14566
theorem OAI.MomentMatrix.integral_trace_cs line 14580
theorem OAI.MomentMatrix.integral_form_cs line 14597
abbrev OAI.DensityEnergy.Space line 14618
def OAI.DensityEnergy.e line 14619
def OAI.DensityEnergy.grad line 14620
def OAI.DensityEnergy.gamma line 14621
def OAI.DensityEnergy.A line 14623
lemma OAI.DensityEnergy.grad_mul line 14626
lemma OAI.DensityEnergy.gamma_symm line 14632
lemma OAI.DensityEnergy.gamma_nonneg line 14636
lemma OAI.DensityEnergy.smooth_gamma line 14640
lemma OAI.DensityEnergy.compact_gamma_left line 14650
lemma OAI.DensityEnergy.gamma_mul_left line 14655
lemma OAI.DensityEnergy.gamma_cutoff_square line 14663
lemma OAI.DensityEnergy.cutoff_young line 14671
theorem OAI.DensityEnergy.caccioppoli line 14687
def OAI.SmoothCutoff.base line 14736
def OAI.SmoothCutoff.cutoff line 14737
lemma OAI.SmoothCutoff.base_smooth line 14739
lemma OAI.SmoothCutoff.smooth line 14741
lemma OAI.SmoothCutoff.nonneg line 14744
lemma OAI.SmoothCutoff.le_one line 14745
lemma OAI.SmoothCutoff.even line 14746
lemma OAI.SmoothCutoff.eq_one line 14750
lemma OAI.SmoothCutoff.eq_zero line 14756
lemma OAI.SmoothCutoff.compact line 14762
lemma OAI.SmoothCutoff.first line 14769
lemma OAI.SmoothCutoff.second line 14779
lemma OAI.SmoothCutoff.base_first_bound line 14795
lemma OAI.SmoothCutoff.base_second_bound line 14801
lemma OAI.SmoothCutoff.derivative_bounds line 14809
lemma OAI.SmoothCutoff.eventually_one line 14830
lemma OAI.SmoothCutoff.first_zero_inside line 14835
lemma OAI.SmoothCutoff.second_zero_inside line 14840
lemma OAI.DensityEnergy.D_eventuallyEq line 14856
lemma OAI.DensityEnergy.A_congr line 14861
lemma OAI.DensityEnergy.grad_congr line 14871
lemma OAI.DensityEnergy.grad_zero_of_not_tsupport line 14876
lemma OAI.DensityEnergy.extend_integration line 14885
lemma OAI.DensityEnergy.harmonic_test line 14918
lemma OAI.DensityEnergy.grad_le line 14933
lemma OAI.DensityEnergy.gamma_upper line 14938
lemma OAI.DensityEnergy.cutoff_gamma_bound line 14957
def OAI.SmoothCutoff.seq line 14979
lemma OAI.SmoothCutoff.seq_smooth line 14981
lemma OAI.SmoothCutoff.seq_compact line 14982
lemma OAI.SmoothCutoff.seq_nonneg line 14983
lemma OAI.SmoothCutoff.seq_le_one line 14984
lemma OAI.SmoothCutoff.seq_eventually line 14986
lemma OAI.SmoothCutoff.seq_derivative_bounds line 14997
lemma OAI.SmoothCutoff.integrable_of_cutoff_bound line 15012
lemma OAI.DensityEnergy.energy_estimate line 15050
lemma OAI.DensityEnergy.eigen_energy_integrable line 15086
lemma OAI.DensityEnergy.DD_mul line 15125
lemma OAI.DensityEnergy.gamma_sum line 15136
lemma OAI.DensityEnergy.A_mul line 15143
lemma OAI.DensityEnergy.gamma_pow_left line 15171
lemma OAI.DensityEnergy.A_pow_succ line 15182
lemma OAI.DensityEnergy.smooth_A line 15199
lemma OAI.DensityEnergy.compact_A line 15209
lemma OAI.DensityEnergy.entries_bound line 15215
lemma OAI.DensityEnergy.second_coordinate line 15233
lemma OAI.DensityEnergy.second_coordinate_bound line 15240
lemma OAI.DensityEnergy.A_bound line 15248
lemma OAI.DensityEnergy.cutoff_A_bound line 15275
lemma OAI.DensityEnergy.gamma_cs line 15302
lemma OAI.DensityEnergy.eigen_cutoff_square_bound line 15313
lemma OAI.DensityEnergy.cutoff_product_eventually line 15333
lemma OAI.DensityEnergy.eigen_graph_integrals line 15345
lemma OAI.DensityEnergy.cutoff_eventually_dominate line 15410
lemma OAI.DensityEnergy.harmonic_energy_zero line 15424
lemma OAI.DensityEnergy.fderiv_zero_of_grad_zero line 15469
theorem OAI.DensityEnergy.harmonic_constant line 15480
lemma OAI.MomentMatrix.trace_conjugate_eq_zero line 15508
lemma OAI.DensityLimit.zero_of_local_limit line 15545
def OAI.DensityEnergy.henergy line 15584
lemma OAI.DensityEnergy.henergy_nonneg line 15587
lemma OAI.DensityEnergy.smooth_henergy line 15593
lemma OAI.DensityEnergy.compact_henergy line 15608
lemma OAI.DensityEnergy.hess_congr line 15616
lemma OAI.DensityEnergy.eigen_hessian_zero line 15621
theorem OAI.DensityEnergy.eigen_linear line 15656
lemma OAI.DensityEnergy.compact_pow_succ line 15683
lemma OAI.DensityEnergy.kernel_cutoff_pointwise line 15688
lemma OAI.DensityEnergy.kernel_A_square_integrable line 15718
lemma OAI.DensityEnergy.A_zero_of_not_tsupport line 15804
lemma OAI.DensityEnergy.local_symmetry line 15815
lemma OAI.DensityEnergy.weak_kernel_of_eigen line 15851
lemma OAI.DensityEnergy.A_sub line 15869
theorem OAI.DensityEnergy.smooth_kernel_affine line 15879
theorem OAI.DensityEnergy.smooth_even_kernel_constant line 15918
lemma OAI.MomentKernel.A_eq_density line 15950
lemma OAI.MomentKernel.smooth_tau line 15963
lemma OAI.MomentKernel.smooth_flux line 15967
lemma OAI.MomentKernel.compact_flux line 15972
lemma OAI.MomentKernel.integration_formula line 15978
lemma OAI.MomentKernel.henergy_eq line 15997
lemma OAI.MomentKernel.hessian_identity line 16010
theorem OAI.MomentKernel.smooth_kernel_affine line 16036
theorem OAI.MomentKernel.integration_by_parts_rightcompact line 16060
lemma OAI.MomentKernel.integration_formula_rightcompact line 16095
lemma OAI.MomentKernel.A_selfadjoint_onecompact line 16122
lemma OAI.MomentKernel.P_selfadjoint_onecompact line 16136
lemma OAI.MomentKernel.smooth_weak_kernel_equation line 16177
lemma OAI.MomentKernel.matrix_A_eq line 16205
theorem OAI.MomentKernel.weak_kernel_smooth line 16208
theorem OAI.MomentKernel.weak_kernel_affine line 16236
lemma OAI.RealSmoothOperator.derivative_add line 16277
lemma OAI.RealSmoothOperator.derivative_smul line 16290
lemma OAI.RealSmoothOperator.operator_add line 16303
lemma OAI.RealSmoothOperator.operator_smul line 16317
def OAI.RealSmoothOperator.tests line 16329
lemma OAI.RealSmoothOperator.tests_smooth line 16335
lemma OAI.RealSmoothOperator.tests_compact line 16336
def OAI.RealSmoothOperator.operatorLinear line 16338
def OAI.RealSmoothOperator.squareLinear line 16343
lemma OAI.RealSmoothOperator.squareLinear_coe line 16346
def OAI.RealSmoothOperator.testsLp line 16351
lemma OAI.RealSmoothOperator.testsLp_coe line 16354
def OAI.RealSmoothOperator.testsLpLinear line 16357
def OAI.RealSmoothOperator.squareLp line 16373
def OAI.RealSmoothOperator.squareRange line 16376
lemma OAI.RealSmoothOperator.squareLp_coe line 16378
lemma OAI.RealSmoothOperator.orthogonal_weak line 16381
abbrev OAI.EvenClosure.Space line 16402
lemma OAI.EvenClosure.pair_affine_zero line 16405
theorem OAI.EvenClosure.mem_closure_of_affine_orthogonal line 16425
lemma OAI.MomentKernel.target_integral_reflect line 16455
theorem OAI.MomentKernel.centered_even_mem_closure line 16466
theorem OAI.SteinExtension.extend line 16503
abbrev OAI.MetricTensor.Idx line 16576
abbrev OAI.MetricTensor.Tensor line 16577
def OAI.MetricTensor.kernel line 16579
def OAI.MetricTensor.pair line 16581
def OAI.MetricTensor.sq line 16582
def OAI.MetricTensor.sw line 16584
def OAI.MetricTensor.cy line 16590
def OAI.MetricTensor.swap line 16596
def OAI.MetricTensor.cycle line 16597
def OAI.MetricTensor.sym line 16598
lemma OAI.MetricTensor.pair_expand line 16600
lemma OAI.MetricTensor.kernel_symm line 16610
lemma OAI.MetricTensor.pair_comm line 16616
lemma OAI.MetricTensor.sq_nonneg line 16628
lemma OAI.MetricTensor.pair_comp line 16632
lemma OAI.MetricTensor.pair_swap line 16642
lemma OAI.MetricTensor.pair_cycle line 16649
lemma OAI.MetricTensor.pair_add_left line 16656
lemma OAI.MetricTensor.pair_add_right line 16659
lemma OAI.MetricTensor.pair_smul_left line 16662
lemma OAI.MetricTensor.pair_smul_right line 16665
lemma OAI.MetricTensor.sq_add line 16669
lemma OAI.MetricTensor.sq_sub line 16674
lemma OAI.MetricTensor.sq_smul line 16681
lemma OAI.MetricTensor.cycle_swap_of_last line 16688
lemma OAI.MetricTensor.swap_cycle_of_last line 16693
lemma OAI.MetricTensor.pair_cyc_eq line 16697
lemma OAI.MetricTensor.pair_swap_cyc line 16701
lemma OAI.MetricTensor.sq_sym line 16705
lemma OAI.MetricTensor.pair_sym line 16714
theorem OAI.MetricTensor.tensor_squares line 16724
theorem OAI.MetricTensor.remainder_nonneg line 16734
def OAI.MetricTensor.act line 16742
lemma OAI.MetricTensor.act_apply line 16745
lemma OAI.MetricTensor.act_comp line 16756
lemma OAI.MetricTensor.act_dot line 16761
lemma OAI.MetricTensor.pair_act line 16768
lemma OAI.MetricTensor.swap_act line 16774
lemma OAI.MetricTensor.act_last_symm line 16788
lemma OAI.MetricTensor.cycle_act line 16802
lemma OAI.MetricTensor.dot_swap line 16823
lemma OAI.MetricTensor.dot_cycle line 16825
lemma OAI.MetricTensor.pair_J line 16829
lemma OAI.MetricTensor.sq_J line 16834
lemma OAI.MetricTensor.pair_J_swap line 16840
lemma OAI.MetricTensor.act_one_one line 16846
lemma OAI.MetricTensor.dot_slot₂ line 16850
lemma OAI.MetricTensor.dot_slot₃ line 16854
lemma OAI.MetricTensor.invariant_cross line 16858
lemma OAI.MetricTensor.invariant_derivative line 16868
theorem OAI.MetricTensor.invariant_remainder_nonneg line 16880
def OAI.TensorEstimate.cube line 16902
def OAI.TensorEstimate.pulledH line 16905
def OAI.TensorEstimate.Q line 16907
lemma OAI.TensorEstimate.cube_swap line 16910
lemma OAI.TensorEstimate.cube_cycle line 16914
lemma OAI.TensorEstimate.cube_last line 16919
lemma OAI.TensorEstimate.act₃_apply line 16924
lemma OAI.TensorEstimate.act₁₃_apply line 16927
lemma OAI.TensorEstimate.act₁₂_apply line 16930
lemma OAI.TensorEstimate.act₂₃_apply line 16933
lemma OAI.TensorEstimate.smooth_pulledH line 16937
lemma OAI.TensorEstimate.derivative_h line 16942
lemma OAI.TensorEstimate.derivative_P_swap line 16951
lemma OAI.TensorEstimate.smooth_Q line 16984
lemma OAI.TensorEstimate.derivative_Q line 16989
def OAI.TensorEstimate.slice line 17051
lemma OAI.TensorEstimate.cubic_trace line 17055
lemma OAI.TensorEstimate.cube_eq_C line 17080
def OAI.TensorEstimate.cross line 17085
def OAI.TensorEstimate.qder line 17088
def OAI.TensorEstimate.cubic line 17092
lemma OAI.TensorEstimate.cross_eq line 17095
lemma OAI.TensorEstimate.qder_eq line 17103
lemma OAI.TensorEstimate.cubic_eq line 17113
theorem OAI.TensorEstimate.pointwise_remainder line 17123
lemma OAI.MomentTrace.cyclic_four line 17143
lemma OAI.MomentTrace.expansion line 17148
lemma OAI.MomentTrace.inverse_sandwich line 17164
lemma OAI.MomentTrace.coefficient_identity line 17169
lemma OAI.MomentTrace.base_identity line 17176
lemma OAI.MomentTrace.trace_contract_symm line 17182
lemma OAI.MomentTrace.H_expansion line 17193
lemma OAI.IntegratedTensor.compact_pulledH line 17209
lemma OAI.IntegratedTensor.compact_matrix_mul_left line 17217
lemma OAI.IntegratedTensor.compact_matrix_mul_right line 17223
lemma OAI.IntegratedTensor.smooth_matrix_trace line 17229
lemma OAI.IntegratedTensor.compact_matrix_trace line 17234
lemma OAI.IntegratedTensor.compact_Q line 17238
lemma OAI.IntegratedTensor.smooth_R line 17243
lemma OAI.IntegratedTensor.compact_R line 17247
lemma OAI.IntegratedTensor.smooth_cross line 17253
lemma OAI.IntegratedTensor.compact_cross line 17258
def OAI.IntegratedTensor.rmat line 17265
def OAI.IntegratedTensor.bmat line 17267
def OAI.IntegratedTensor.base line 17270
def OAI.IntegratedTensor.rterm line 17273
def OAI.IntegratedTensor.mixed line 17276
lemma OAI.IntegratedTensor.rmat_symm line 17279
lemma OAI.IntegratedTensor.mixed_integral line 17286
theorem OAI.IntegratedTensor.integration_by_parts_rightcompact line 17324
def OAI.IntegratedTensor.L line 17359
lemma OAI.IntegratedTensor.smooth_L line 17362
lemma OAI.IntegratedTensor.smooth_qder line 17366
lemma OAI.IntegratedTensor.compact_qder line 17372
lemma OAI.IntegratedTensor.smooth_cubic line 17378
lemma OAI.IntegratedTensor.compact_cubic line 17387
def OAI.IntegratedTensor.divterm line 17392
lemma OAI.IntegratedTensor.smooth_divterm line 17395
lemma OAI.IntegratedTensor.compact_divterm line 17401
lemma OAI.IntegratedTensor.divterm_integral line 17406
lemma OAI.IntegratedTensor.smooth_bmat line 17445
lemma OAI.IntegratedTensor.compact_bmat line 17450
lemma OAI.IntegratedTensor.smooth_base line 17455
lemma OAI.IntegratedTensor.compact_base line 17461
lemma OAI.IntegratedTensor.smooth_rterm line 17466
lemma OAI.IntegratedTensor.compact_rterm line 17472
lemma OAI.IntegratedTensor.smooth_mixed line 17478
lemma OAI.IntegratedTensor.compact_mixed line 17482
def OAI.IntegratedTensor.jacW line 17487
def OAI.IntegratedTensor.traceL line 17490
def OAI.IntegratedTensor.traceH line 17493
lemma OAI.IntegratedTensor.traceL_expansion line 17496
lemma OAI.IntegratedTensor.traceH_expansion line 17512
lemma OAI.IntegratedTensor.rterm_nonneg line 17536
lemma OAI.IntegratedTensor.expectation_const_mul line 17542
lemma OAI.IntegratedTensor.expectation_sub line 17547
lemma OAI.IntegratedTensor.expectation_nonneg line 17554
theorem OAI.IntegratedTensor.tensor_estimate line 17558
def OAI.FullTensor.wField line 17608
def OAI.FullTensor.bField line 17611
def OAI.FullTensor.mField line 17614
def OAI.FullTensor.jacobian line 17617
def OAI.FullTensor.squareTrace line 17619
def OAI.FullTensor.hEnergy line 17622
def OAI.FullTensor.wEnergy line 17625
lemma OAI.FullTensor.jacobian_pull line 17628
lemma OAI.FullTensor.squareTrace_pull line 17643
lemma OAI.FullTensor.hEnergy_pull line 17653
lemma OAI.FullTensor.wField_divergence line 17660
lemma OAI.FullTensor.bochner_trace line 17677
theorem OAI.FullTensor.tensor_energy line 17707
lemma OAI.DualEnergy.integral_divergence line 17745
lemma OAI.DualEnergy.smooth_bField line 17755
lemma OAI.DualEnergy.compact_bField line 17761
lemma OAI.DualEnergy.smooth_mField line 17766
lemma OAI.DualEnergy.bField_symm line 17772
lemma OAI.DualEnergy.pairings line 17779
def OAI.DualEnergy.tau line 17829
lemma OAI.DualEnergy.trace_pair_integrable line 17832
lemma OAI.DualEnergy.first_energy_integrable line 17842
lemma OAI.DualEnergy.second_energy_integrable line 17854
lemma OAI.DualEnergy.first_cs line 17866
lemma OAI.DualEnergy.wEnergy_form line 17891
lemma OAI.DualEnergy.second_cs line 17901
lemma OAI.DualEnergy.entries_bound line 17950
lemma OAI.DualEnergy.smooth_tau line 17968
lemma OAI.DualEnergy.fderiv_tau_row line 17972
lemma OAI.DualEnergy.compact_stein line 17976
lemma OAI.DualEnergy.tau_hessian_integrable line 18009
lemma OAI.DualEnergy.homogeneous_trace_moment line 18020
lemma OAI.DualEnergy.trace_energy_subsum line 18081
lemma OAI.DualEnergy.form_subsum line 18087
lemma OAI.DualEnergy.discard_energy line 18091
def OAI.SoftSlab.linear line 18134
lemma OAI.SoftSlab.linear_apply line 18138
lemma OAI.SoftSlab.linear_basis line 18141
def OAI.SoftSlab.summand line 18144
lemma OAI.SoftSlab.summand_eq line 18149
lemma OAI.SoftSlab.smooth_summand line 18153
lemma OAI.SoftSlab.pd_summand line 18156
lemma OAI.SoftSlab.hess_summand line 18167
lemma OAI.SoftSlab.summand_even line 18185
lemma OAI.SoftSlab.summand_nonneg line 18191
lemma OAI.SoftSlab.hess_summand_posSemidef line 18194
lemma OAI.SoftSlab.euler_summand line 18207
lemma OAI.SoftSlab.hessian_euler line 18219
def OAI.SoftSlab.potential line 18239
lemma OAI.SoftSlab.smooth_potential line 18243
lemma OAI.SoftSlab.potential_even line 18250
lemma OAI.SoftSlab.potential_lower line 18258
lemma OAI.SoftSlab.pd_quadratic line 18263
lemma OAI.SoftSlab.hess_quadratic line 18279
lemma OAI.SoftSlab.hess_add line 18288
lemma OAI.SoftSlab.hess_sum line 18296
lemma OAI.SoftSlab.hess_potential line 18305
lemma OAI.SoftSlab.potential_strongly_convex line 18313
lemma OAI.GaussianPolynomial.gaussian_product line 18330
lemma OAI.GaussianPolynomial.monomial_integrable line 18334
lemma OAI.GaussianPolynomial.polynomial_integrable line 18347
lemma OAI.GaussianPolynomial.dominated_polynomial line 18359
lemma OAI.GaussianPolynomial.partition_integrable line 18379
lemma OAI.GaussianPolynomial.normalized_polynomial line 18389
lemma OAI.GaussianPolynomial.partition_pos line 18405
lemma OAI.GaussianPolynomial.normalized_probability line 18410
abbrev OAI.SoftSlab.law line 18429
def OAI.SoftSlab.linearPolynomial line 18433
lemma OAI.SoftSlab.eval_linearPolynomial line 18437
lemma OAI.SoftSlab.potential_partition_pos line 18442
lemma OAI.SoftSlab.potential_probability line 18448
lemma OAI.SoftSlab.polynomial_moment line 18454
lemma OAI.SoftSlab.integrable_summand line 18461
lemma OAI.SoftSlab.integrable_pd_summand line 18468
lemma OAI.SoftSlab.integrable_x_pd_summand line 18474
lemma OAI.SoftSlab.integrable_hess_summand line 18486
lemma OAI.SoftSlab.mean_summand_pos line 18493
lemma OAI.VarianceDuality.quadratic_cs line 18537
lemma OAI.VarianceDuality.weighted_coefficient_cs line 18545
theorem OAI.VarianceDuality.combine_energies line 18558
theorem OAI.VarianceDuality.extend_dual_bound line 18582
theorem OAI.VarianceDuality.variance_from_dense_tests line 18593
lemma OAI.DualEnergy.compact_dual_generic line 18624
theorem OAI.MomentSlab.summand_trace_moment line 18667
theorem OAI.MomentSlab.compact_dual_bound line 18689
lemma OAI.LpVariance.lp_inner line 18745
lemma OAI.LpVariance.lp_norm_sq line 18752
lemma OAI.LpVariance.toLp_inner line 18756
lemma OAI.LpVariance.toLp_norm_sq line 18763
theorem OAI.LpVariance.integral_dual_extend line 18768
def OAI.LpVariance.sumPotential line 18786
def OAI.LpVariance.centered line 18788
lemma OAI.LpVariance.sum_memLp line 18791
lemma OAI.LpVariance.centered_memLp line 18797
lemma OAI.LpVariance.centered_integral line 18800
lemma OAI.LpVariance.centered_sq line 18805
lemma OAI.LpVariance.centered_pair_sum line 18819
theorem OAI.LpVariance.variance_of_centered_dual line 18846
lemma OAI.PositiveDensity.isOpenPos line 18875
lemma OAI.SoftSlab.summand_memLp line 18893
lemma OAI.SoftSlab.potential_nonneg line 18902
lemma OAI.SoftSlab.law_openPos line 18908
lemma OAI.MomentSlab.square_double_divergence line 18921
lemma OAI.MomentSlab.range_dual_bound line 18937
theorem OAI.MomentSlab.variance_from_moment line 18973
def OAI.LogBrunnMinkowski.MainStatement line 19030
lemma OAI.LogBrunnMinkowski.body_nonempty line 19036
lemma OAI.LogBrunnMinkowski.support_attained line 19039
lemma OAI.LogBrunnMinkowski.inner_le_support line 19045
lemma OAI.LogBrunnMinkowski.support_le_iff line 19051
lemma OAI.LogBrunnMinkowski.support_zero line 19061
lemma OAI.LogBrunnMinkowski.support_smul line 19066
lemma OAI.LogBrunnMinkowski.interior_neg_mem line 19077
lemma OAI.LogBrunnMinkowski.zero_mem_interior line 19087
lemma OAI.LogBrunnMinkowski.positive_support line 19095
lemma OAI.LogBrunnMinkowski.mem_wulff_support_iff line 19108
lemma OAI.LogBrunnMinkowski.wulff_support line 19137
lemma OAI.LogBrunnMinkowski.logCombination_zero line 19142
lemma OAI.LogBrunnMinkowski.logCombination_one line 19147
lemma OAI.LogBrunnMinkowski.main_at_zero line 19152
lemma OAI.LogBrunnMinkowski.main_at_one line 19157
lemma OAI.LogBrunnMinkowski.body_volume_pos line 19162
lemma OAI.LogBrunnMinkowski.body_volume_ne_top line 19165
lemma OAI.LogBrunnMinkowski.support_continuous line 19168
lemma OAI.LogBrunnMinkowski.support_neg line 19172
abbrev OAI.LogBrunnMinkowski.UnitSphere line 19184
lemma OAI.LogBrunnMinkowski.unitSphere_nonempty line 19186
def OAI.LogBrunnMinkowski.finiteSlabs line 19191
lemma OAI.LogBrunnMinkowski.finiteSlabs_closed line 19194
lemma OAI.LogBrunnMinkowski.finiteSlabs_compact line 19200
def OAI.LogBrunnMinkowski.directions line 19213
lemma OAI.LogBrunnMinkowski.basis_mem_directions line 19217
lemma OAI.LogBrunnMinkowski.dense_mem_directions line 19223
lemma OAI.LogBrunnMinkowski.directions_unit line 19229
lemma OAI.LogBrunnMinkowski.directions_mono line 19238
lemma OAI.LogBrunnMinkowski.finiteSlabs_antitone line 19244
lemma OAI.LogBrunnMinkowski.iInter_finiteSlabs_eq_wulff line 19249
lemma OAI.LogBrunnMinkowski.tendsto_volume_finiteSlabs line 19274
def OAI.LogBrunnMinkowski.interpolatedSupport line 19285
lemma OAI.LogBrunnMinkowski.interpolatedSupport_sphere_continuous line 19288
lemma OAI.LogBrunnMinkowski.interpolatedSupport_even line 19298
lemma OAI.LogBrunnMinkowski.main_of_finite_slabs line 19304
def OAI.LogBrunnMinkowski.oneEquiv line 19334
def OAI.LogBrunnMinkowski.oneDirection line 19337
lemma OAI.LogBrunnMinkowski.oneDirection_norm line 19339
lemma OAI.LogBrunnMinkowski.inner_oneDirection line 19342
lemma OAI.LogBrunnMinkowski.sphere_one_cases line 19346
lemma OAI.LogBrunnMinkowski.wulff_one_eq line 19357
lemma OAI.LogBrunnMinkowski.volume_wulff_one line 19373
lemma OAI.LogBrunnMinkowski.main_dimension_one line 19381
def OAI.SlabPartition.derivativePoly line 19421
def OAI.SlabPartition.variation line 19424
lemma OAI.SlabPartition.variation_eq line 19428
lemma OAI.SlabPartition.variation_continuous line 19433
lemma OAI.SlabPartition.variation_hasDerivAt line 19437
def OAI.SlabPartition.potential line 19452
def OAI.SlabPartition.density line 19455
def OAI.SlabPartition.densityFirst line 19458
def OAI.SlabPartition.densitySecond line 19461
lemma OAI.SlabPartition.potential_continuous line 19464
lemma OAI.SlabPartition.density_continuous line 19470
lemma OAI.SlabPartition.densityFirst_continuous line 19473
lemma OAI.SlabPartition.densitySecond_continuous line 19477
lemma OAI.SlabPartition.density_hasDerivAt line 19482
lemma OAI.SlabPartition.densityFirst_hasDerivAt line 19490
lemma OAI.SlabPartition.potential_lower line 19498
lemma OAI.SlabPartition.polynomial_integrable line 19505
lemma OAI.SlabPartition.density_integrable line 19511
lemma OAI.SlabPartition.densityFirst_integrable line 19516
lemma OAI.SlabPartition.densitySecond_integrable line 19522
def OAI.SlabPartition.boundPoly line 19532
lemma OAI.SlabPartition.eval_boundPoly line 19536
lemma OAI.SlabPartition.boundPoly_nonneg line 19542
lemma OAI.SlabPartition.norm_variation_le line 19549
lemma OAI.SlabPartition.density_le_gaussian line 19573
lemma OAI.SlabPartition.norm_densityFirst_le line 19579
lemma OAI.SlabPartition.norm_densitySecond_le line 19590
def OAI.SlabPartition.partition line 19613
def OAI.SlabPartition.partitionFirst line 19616
def OAI.SlabPartition.partitionSecond line 19619
lemma OAI.SlabPartition.partition_pos line 19622
lemma OAI.SlabPartition.partition_hasDerivAt line 19626
lemma OAI.SlabPartition.partitionFirst_hasDerivAt line 19638
lemma OAI.SlabPartition.log_partition_hasDerivAt line 19651
lemma OAI.SlabPartition.log_partition_derivative_hasDerivAt line 19657
def OAI.SlabPartition.mean line 19666
def OAI.SlabPartition.variance line 19669
lemma OAI.SlabPartition.variance_eq line 19673
lemma OAI.SlabPartition.partitionFirst_eq line 19702
lemma OAI.SlabPartition.partitionSecond_eq line 19706
lemma OAI.SlabPartition.log_partition_second line 19719
lemma OAI.SlabPartition.log_partition_concave_of_variance line 19732
lemma OAI.SlabPartition.partition_rpow_le_of_variance line 19749
lemma OAI.SoftSlabLimits.level_null line 19774
lemma OAI.SoftSlabLimits.abs_level_ne_ae line 19789
def OAI.SoftSlabLimits.body line 19801
def OAI.SoftSlabLimits.gaussian line 19804
def OAI.SoftSlabLimits.density line 19807
lemma OAI.SoftSlabLimits.body_measurable line 19810
lemma OAI.SoftSlabLimits.continuous_density line 19817
lemma OAI.SoftSlabLimits.density_le_gaussian line 19822
lemma OAI.SoftSlabLimits.gaussian_integrable line 19828
lemma OAI.SoftSlabLimits.evenIndex_tendsto line 19833
lemma OAI.SoftSlabLimits.density_tendsto line 19836
lemma OAI.SoftSlabLimits.partition_tendsto line 19871
lemma OAI.SoftSlabLimits.gaussian_tendsto_volume line 19882
lemma OAI.SoftSlabLimits.volume_rpow_le_of_partition line 19900
def OAI.SlabReduction.linearPoly line 19933
def OAI.SlabReduction.feature line 19936
lemma OAI.SlabReduction.eval_feature line 19939
def OAI.SlabReduction.width line 19943
def OAI.SlabReduction.normal line 19945
lemma OAI.SlabReduction.normal_apply line 19948
def OAI.SlabReduction.rate line 19951
lemma OAI.SlabReduction.width_pos line 19953
lemma OAI.SlabReduction.width_exponential line 19956
lemma OAI.SlabReduction.feature_exponential line 19965
def OAI.SlabReduction.features line 19975
def OAI.SlabReduction.rates line 19978
def OAI.SlabReduction.normals line 19980
def OAI.SlabReduction.widths line 19983
lemma OAI.SlabReduction.features_nonneg line 19986
lemma OAI.SlabReduction.variation_identification line 19992
lemma OAI.SlabReduction.density_identification line 20003
lemma OAI.SlabReduction.widths_zero line 20016
lemma OAI.SlabReduction.widths_one line 20022
theorem OAI.SlabReduction.finite_slabs_of_variance line 20027
lemma OAI.LogBrunnMinkowski.finiteSlabs_preimage_eq_body line 20052
lemma OAI.LogBrunnMinkowski.volume_finiteSlabs_eq_body line 20070
lemma OAI.LogBrunnMinkowski.ennreal_rpow_le_of_toReal line 20079
lemma OAI.LogBrunnMinkowski.finiteSlabs_volume_of_body_inequality line 20087
lemma OAI.LogBrunnMinkowski.volume_body_finiteSlabs_ne_top line 20109
lemma OAI.LogBrunnMinkowski.finiteSlabs_volume_of_variance line 20117
def OAI.LogBrunnMinkowski.SoftVarianceStatement line 20144
lemma OAI.LogBrunnMinkowski.varying_density_eq line 20154
lemma OAI.LogBrunnMinkowski.varying_variation_eq line 20173
lemma OAI.LogBrunnMinkowski.source_variance_at_parameter line 20187
lemma OAI.LogBrunnMinkowski.main_of_softVariance line 20208
lemma OAI.SchwartzKernel.integral_eq_fourier_zero line 20246
lemma OAI.SchwartzKernel.integral_fourierInv line 20251
lemma OAI.SchwartzKernel.integral_derivative line 20254
lemma OAI.SchwartzKernel.derivative_bound line 20261
theorem OAI.SchwartzKernel.hasFDerivAt_convolution line 20265
lemma OAI.ScaledKernel.change_variables line 20300
def OAI.ScaledKernel.dilate line 20307
lemma OAI.ScaledKernel.dilate_apply line 20311
lemma OAI.ScaledKernel.dilate_fderiv line 20315
def OAI.ScaledKernel.applyKernel line 20324
lemma OAI.ScaledKernel.apply_eq line 20327
lemma OAI.ScaledKernel.derivative line 20336
def OAI.AnnularSymbol.bump line 20366
def OAI.AnnularSymbol.cutoff line 20367
lemma OAI.AnnularSymbol.contDiff_cutoff line 20369
lemma OAI.AnnularSymbol.compact_cutoff line 20371
lemma OAI.AnnularSymbol.cutoff_zero_near line 20373
def OAI.AnnularSymbol.multiplier line 20385
lemma OAI.AnnularSymbol.multiplier_compact line 20387
lemma OAI.AnnularSymbol.multiplier_smooth line 20390
def OAI.AnnularSymbol.symbol line 20403
def OAI.AnnularSymbol.kernel line 20408
lemma OAI.AnnularSymbol.symbol_zero line 20412
lemma OAI.AnnularSymbol.inverse_identity line 20418
def OAI.AnnularFourier.product line 20437
lemma OAI.AnnularFourier.product_apply line 20439
def OAI.AnnularFourier.conv line 20441
lemma OAI.AnnularFourier.fourier_conv line 20442
lemma OAI.AnnularFourier.fourier_dilate line 20445
lemma OAI.AnnularFourier.fourier_second line 20457
def OAI.AnnularFourier.elliptic line 20468
lemma OAI.AnnularFourier.quadratic_sum line 20472
lemma OAI.AnnularFourier.fourier_elliptic line 20482
def OAI.AnnularFourier.normalized line 20495
lemma OAI.AnnularFourier.fourier_normalized line 20498
lemma OAI.AnnularFourier.normalized_conv line 20503
def OAI.AnnularFourier.annulus line 20513
lemma OAI.AnnularFourier.annulus_apply line 20517
lemma OAI.AnnularFourier.inverse_scaled line 20520
theorem OAI.AnnularFourier.annular_identity line 20535
def OAI.AnnularFourier.lowBump line 20559
def OAI.AnnularFourier.lowSymbol line 20560
lemma OAI.AnnularFourier.lowSymbol_apply line 20565
lemma OAI.AnnularFourier.lowSymbol_zero line 20567
lemma OAI.AnnularFourier.lowSymbol_bound line 20571
lemma OAI.AnnularFourier.annulus_low line 20576
def OAI.AnnularFourier.lowFilter line 20581
lemma OAI.AnnularFourier.lowFilter_tendsto line 20584
lemma OAI.AnnularFourier.inverse_sub line 20608
lemma OAI.AnnularFourier.piece_telescope line 20611
lemma OAI.VectorKernelHolder.rpow_bound line 20629
lemma OAI.VectorKernelHolder.integrable_moment line 20640
theorem OAI.VectorKernelHolder.cancellation_bound line 20652
lemma OAI.ScaleSeries.summable_bound line 20691
lemma OAI.ScaleSeries.tail_bound line 20698
lemma OAI.ScaleSeries.finite_bound line 20715
theorem OAI.ScaleSeries.modulus_sum line 20732
lemma OAI.KernelSeries.apply_bound line 20762
lemma OAI.KernelSeries.derivative_bound line 20770
lemma OAI.KernelSeries.lipschitz_bound line 20784
theorem OAI.KernelSeries.holder_sum line 20796
def OAI.AnnularFourier.lowKernel line 20852
lemma OAI.AnnularFourier.decompose line 20855
lemma OAI.AnnularFourier.lowFilter_eq_kernel line 20883
lemma OAI.AnnularFourier.lowFilter_lipschitz line 20896
theorem OAI.AnnularFourier.schwartz_schauder line 20921
lemma OAI.KernelCommutator.integrable_mul line 20963
lemma OAI.KernelCommutator.apply_bound line 20973
def OAI.KernelCommutator.anchored line 20986
def OAI.KernelCommutator.commutator line 20989
lemma OAI.KernelCommutator.commutator_bound line 20992
lemma OAI.KernelCommutator.integrable_weighted_derivative line 21016
lemma OAI.KernelCommutator.anchored_derivative_bound line 21027
lemma OAI.ScaledKernel.holder_apply line 21087
lemma OAI.ScaledKernel.apply_tendsto line 21106
def OAI.CompactMollification.dd line 21131
lemma OAI.CompactMollification.conv_eq line 21133
lemma OAI.CompactMollification.normalized_compact line 21147
lemma OAI.CompactMollification.apply_compact line 21151
lemma OAI.CompactMollification.apply_smooth line 21157
lemma OAI.CompactMollification.apply_derivative line 21164
lemma OAI.CompactMollification.derivative_compact line 21175
lemma OAI.CompactMollification.derivative_C1 line 21180
lemma OAI.CompactMollification.apply_second line 21184
lemma OAI.CompactMollification.dd_continuous line 21194
lemma OAI.CompactMollification.dd_compact line 21198
lemma OAI.CompactMollification.dd_schwartz line 21201
def OAI.CompactMollification.mollifier line 21208
lemma OAI.CompactMollification.mollifier_compact line 21212
lemma OAI.CompactMollification.mollifier_integral line 21215
lemma OAI.CompactMollification.mollifier_norm line 21219
def OAI.CompactMollification.elliptic line 21231
lemma OAI.CompactMollification.bounded_compact line 21235
lemma OAI.CompactMollification.elliptic_continuous line 21242
lemma OAI.CompactMollification.elliptic_compact line 21246
lemma OAI.CompactMollification.elliptic_schwartz line 21259
lemma OAI.CompactMollification.apply_elliptic line 21263
theorem OAI.CompactMollification.compact_schauder line 21273
lemma OAI.ScalarInterpolation.second_bound line 21319
def OAI.HessianInterpolation.hessian line 21388
lemma OAI.HessianInterpolation.ray_second line 21390
lemma OAI.HessianInterpolation.diagonal_bound line 21398
theorem OAI.HessianInterpolation.norm_bound line 21433
lemma OAI.HessianInterpolation.bilinear_norm_bound line 21462
lemma OAI.CompactMollification.dd_hessian line 21505
theorem OAI.CompactMollification.hessian_schauder line 21514
def OAI.CoefficientTrace.trace line 21561
lemma OAI.CoefficientTrace.sub_left line 21563
lemma OAI.CoefficientTrace.sub_right line 21566
lemma OAI.CoefficientTrace.norm_bound line 21569
lemma OAI.CoefficientTrace.variation line 21582
lemma OAI.CoefficientTrace.holder_error line 21589
theorem OAI.HolderAbsorption.improve line 21617
lemma OAI.CompactMollification.elliptic_trace line 21649
theorem OAI.CompactMollification.variable_schauder line 21654
lemma OAI.HessianInterpolation.hessian_comp line 21736
def OAI.HessianInterpolation.complexLift line 21747
lemma OAI.HessianInterpolation.complexLift_apply line 21749
lemma OAI.HessianInterpolation.complexLift_sub line 21751
lemma OAI.HessianInterpolation.complexLift_norm line 21755
lemma OAI.HessianInterpolation.complexLift_dist line 21773
lemma OAI.HessianInterpolation.hessian_complex line 21775
lemma OAI.CompactMollification.trace_complex line 21786
theorem OAI.CompactMollification.real_variable_schauder line 21791
lemma OAI.HolderLocalization.of_lipschitz_bounded line 21837
lemma OAI.HolderLocalization.bilinear_holder line 21856
lemma OAI.HolderLocalization.cutoff_holder line 21879
lemma OAI.HolderLocalization.localized_bilinear line 21910
def OAI.HolderControl.Controlled line 21953
lemma OAI.HolderControl.Controlled.add line 21958
lemma OAI.HolderControl.Controlled.localized_bilinear line 21969
lemma OAI.HolderControl.Controlled.of_single line 21984
lemma OAI.HolderControl.Controlled.congr line 21990
lemma OAI.HolderControl.compact_C1 line 22002
lemma OAI.HessianInterpolation.hessian_mul line 22020
lemma OAI.HolderControl.Controlled.trace line 22045
lemma OAI.HolderControl.Controlled.reindex line 22076
theorem OAI.HolderControl.localized_family line 22082
lemma OAI.HolderControl.Controlled.mono line 22177
lemma OAI.HolderControl.const line 22183
lemma OAI.HolderControl.Controlled.sub line 22187
lemma OAI.HolderControl.Controlled.linear line 22197
lemma OAI.HolderControl.Controlled.bilinear line 22208
lemma OAI.HolderControl.extend_field line 22226
theorem OAI.HolderControl.interior_family line 22257
theorem OAI.HolderControl.interior_ball line 22285
lemma OAI.HessianTrace.scalar_hessian line 22336
lemma OAI.HessianTrace.trace_eq_matrix line 22348
def OAI.HessianTrace.fromMatrix line 22367
lemma OAI.HessianTrace.fromMatrix_toMatrix line 22370
lemma OAI.HessianTrace.hessian_clm line 22378
lemma OAI.HessianTrace.holder_transfer line 22384
lemma OAI.HessianTrace.toMatrix_fromMatrix line 22410
lemma OAI.HessianTrace.inner_pos_fromMatrix line 22415
def OAI.LogDetSegment.segmentMatrix line 22448
lemma OAI.LogDetSegment.segment_pos line 22451
lemma OAI.LogDetSegment.segment_continuous line 22463
lemma OAI.LogDetSegment.segment_inverse_continuous line 22467
lemma OAI.LogDetSegment.hasDerivAt_logdet_segment line 22475
def OAI.LogDetSegment.meanInverse line 22495
def OAI.LogDetSegment.traceRight line 22497
lemma OAI.LogDetSegment.logdet_difference line 22503
lemma OAI.LogDetSegment.matrix_norm_mul line 22527
lemma OAI.LogDetSegment.inverse_sub line 22541
lemma OAI.LogDetSegment.inverse_lipschitz line 22546
lemma OAI.LogDetSegment.mean_inverse_dist line 22560
lemma OAI.LogDetSegment.segment_dist line 22583
lemma OAI.LogDetSegment.mean_inverse_holder line 22592
lemma OAI.LogDetSegment.mean_inverse_self line 22614
lemma OAI.LogDetSegment.mean_inverse_close line 22617
lemma OAI.LogDetSegment.mean_inverse_norm line 22645
lemma OAI.LogDetSegment.compact_segment_inverse_bound line 22652
lemma OAI.HolderControl.compact_convex_C1 line 22679
lemma OAI.LogDetSegment.local_mean_control line 22709
def OAI.FiniteDifference.increment line 22780
lemma OAI.FiniteDifference.hasDerivAt_ray line 22783
lemma OAI.FiniteDifference.ray_integrable line 22790
lemma OAI.FiniteDifference.increment_integral line 22795
lemma OAI.FiniteDifference.ray_mem line 22802
lemma OAI.FiniteDifference.increment_holder line 22808
lemma OAI.FiniteDifference.increment_bound line 22828
def OAI.FiniteDifference.normalized line 22845
lemma OAI.FiniteDifference.normalized_controlled line 22847
lemma OAI.FiniteDifference.fderiv_normalized line 22872
def OAI.MomentQuotient.quotient line 22892
def OAI.MomentQuotient.matrixHessian line 22894
def OAI.MomentQuotient.coefficient line 22897
lemma OAI.MomentQuotient.quotient_contDiff line 22901
lemma OAI.MomentQuotient.hessian_quotient line 22906
lemma OAI.MomentQuotient.toMatrix_coefficient line 22920
lemma OAI.MomentQuotient.equation line 22927
lemma OAI.MomentQuotient.quotient_normalized line 22956
lemma OAI.MomentQuotient.derivative_gradient line 22959
lemma OAI.MomentQuotient.source_derivative_controlled line 22966
lemma OAI.MomentQuotient.normalized_hessian_finite line 22990
lemma OAI.MomentQuotient.data line 23005
lemma OAI.AEDerivativeLocal.increment_bound line 23046
theorem OAI.AEDerivativeLocal.hasFDerivAt_of_ae line 23083
lemma OAI.QuotientBootstrap.derivative_holder line 23112
theorem OAI.QuotientBootstrap.contDiffOn_one_of_quotients line 23144
theorem OAI.FiniteDifference.C1_of_controlled_normalized line 23207
theorem OAI.MomentQuotient.C3_local line 23261
def OAI.CoefficientTrace.bilinear line 23351
lemma OAI.CoefficientTrace.bilinear_apply line 23359
lemma OAI.LinearSchauder.quotient_equation line 23374
theorem OAI.LinearSchauder.C3_local line 23398
def OAI.HolderJets.Local line 23491
lemma OAI.HolderJets.Local.of_C1 line 23494
lemma OAI.HolderJets.restrict_exponent line 23501
lemma OAI.HolderJets.Local.common line 23517
lemma OAI.HolderJets.Local.linear line 23531
lemma OAI.HolderJets.Local.add line 23537
lemma OAI.HolderJets.Local.bilinear line 23543
lemma OAI.HolderJets.Local.comp_C1 line 23550
def OAI.HolderJets.Regular line 23579
lemma OAI.HolderJets.Regular.contDiff line 23586
lemma OAI.HolderJets.Regular.continuous line 23594
lemma OAI.HolderJets.Regular.local line 23596
lemma OAI.HolderJets.Regular.pred line 23601
lemma OAI.HolderJets.Regular.linear line 23607
lemma OAI.HolderJets.Regular.add line 23617
lemma OAI.HolderJets.Regular.bilinear line 23626
lemma OAI.HolderJets.Regular.comp_smooth line 23638
lemma OAI.HolderJets.Regular.of_Cnext line 23653
lemma OAI.HolderJets.Regular.of_smooth line 23659
lemma OAI.HolderJets.Regular.mono line 23662
lemma OAI.HolderJets.Regular.prod line 23674
lemma OAI.HolderJets.Regular.sum line 23680
lemma OAI.HolderJets.Regular.clm_of_basis line 23689
lemma OAI.HessianDirectional.derivative_direction line 23713
lemma OAI.LinearSchauder.regular_three line 23761
lemma OAI.LinearSchauder.differentiated_equation line 23794
theorem OAI.LinearSchauder.higher line 23815
def OAI.MomentSchauder.scalarToVector line 23857
def OAI.MomentSchauder.scalarToMatrix line 23861
lemma OAI.MomentSchauder.scalarToVector_hessian line 23865
lemma OAI.MomentSchauder.scalarToMatrix_hessian line 23872
lemma OAI.MomentSchauder.inverse_smooth_at line 23880
lemma OAI.MomentSchauder.trace_scalar_matrix line 23909
lemma OAI.MomentSchauder.equation line 23918
theorem OAI.MomentSchauder.smooth_of_regular_three line 23967
theorem OAI.CompactMomentVariational.C2_to_smooth line 24019
def OAI.MomentCoordinatesBridge.coord line 24073
def OAI.MomentCoordinatesBridge.ob line 24074
lemma OAI.MomentCoordinatesBridge.coord_basis line 24075
lemma OAI.MomentCoordinatesBridge.grad_pull line 24078
lemma OAI.MomentCoordinatesBridge.pd_pull line 24088
lemma OAI.MomentCoordinatesBridge.hess_pull line 24092
lemma OAI.SoftEuclidean.convex_summand line 24121
lemma OAI.SoftEuclidean.convex_sum line 24127
lemma OAI.SoftEuclidean.midpoint_curvature line 24134
lemma OAI.SoftEuclidean.convex_potential line 24149
lemma OAI.SoftEuclidean.integrable_potential line 24161
lemma OAI.MomentHessianCap.inner_cap line 24175
lemma OAI.MomentHessianCap.matrix_cap line 24188
lemma OAI.MomentHessianCap.positive_derivative line 24206
lemma OAI.PositiveDiffeomorphism.injective line 24232
theorem OAI.PositiveDiffeomorphism.exists_homeomorph line 24251
lemma OAI.MeasureCoordinates.map_density line 24279
lemma OAI.MomentCoordinatesBridge.coord_integral line 24295
lemma OAI.MomentCoordinatesBridge.coord_density line 24298
lemma OAI.MomentCoordinatesBridge.coord_source line 24302
lemma OAI.MomentCoordinatesBridge.coord_normalized line 24309
theorem OAI.ActualMoment.euclidean line 24328
theorem OAI.ActualMoment.coordinates line 24370
lemma OAI.ActualMoment.feature_eval line 24416
lemma OAI.ActualMoment.density_eq line 24420
lemma OAI.ActualMoment.mean_eq line 24427
lemma OAI.ActualMoment.variance_eq line 24437
lemma OAI.ActualMoment.covariance_rhs line 24452
theorem OAI.LogBrunnMinkowski.softVariance line 24468
theorem OAI.LogBrunnMinkowski.main line 24481
Distinct definitions of this name: ComparatorChallenges/LogBrunnMinkowski.lean:30 (same statement text; different proof or body). Qualify references as OAI.LogBrunnMinkowski.main@path.