L'axiome d'univalence | Infini 25

[@valentino76600]

Des que tu as prononcé "ascenseur", je l'ai attendu et tu l'as dit : "monter vers le haut" ..! Magnifique haha !

[@lordkay-9874]

J'ai 15 ans je te suis mais je ne te suis en rien dans tes vidéos c'est vraiment au dessus de mes capacités pour l'instant mais à chaque épisode au moins j'essaye de comprendre :)

[@adfr1806]

LordKAY /-\\/\/ pareil maintenant j’ai 16 ans

[@cyrilpujol2047]

Exellente vidéo! J'adore tes épisodes, car je trouve que même quand il y a des choses que l'on ne comprend pas exactement directement (/pas) c'est extrêmement intéressant d'essayer de voir les liens entre les objets même quand il nous manque une étape , ou d'essayer de comprendre à quoi correspond un mot de vocabulaire.C est hyper stimulant et je suis sur que ça entraîne à mieux comprendre des explications en général. Tu es une des seules chaînes (voir la seule) que je connaisse qui traite d'un niveau aussi élevé, et c'est agréable de vraiment apprendre des choses complètement différentes et vraiment en détail. Bref tu es le meilleur

[@mathieumontin639]

Salut Lê. Merci pour ces épisodes sur l'infini qui permettent d'introduire la théorie des types. A la fin de cet épisode, tu présentes l'outil coq et son interface (coqide) pas très élaborée. il existe aussi proofgeneral (au sein d'Emacs) qui permet de faire du coq un peu plus intuitivement. Et comme outil tu devrais jeter un oeil à Agda ! Il est basé sur la même théorie des types mais propose de créer ses lambda-termes à la main, à l'aide d'un mode emacs qui guide la preuve / le développement. Cela pourrait t'intéresser, d'autant plus qu'Agda supporte l'unicode et les notations infixes ce qui donne aux programmes Agda un aspect beaucoup plus mathématique visuellement que coq.

[@Secifelam]

Merci pour toutes les vidéos que j'ai appréciées, mais je vais maintenant te laisser et je te souhaite plein de réussites. Au revoir Lê.

[@maximeeuziere]

dur à intuiter, mais facile à retweeter

[@lerouxstephane6758]

Bonjour, je viens de comprendre un truc sur le cercle \o/. En fait, en voyant la description du cercle S1, j'avais l'impression qu'il n'avait qu'un unique point : sa base. Et bien non. Enfin si, mais non. Bref, on peut montrer la propriété suivante sur S1 : non-(pour tout x de S1, base = x) (ne pouvant pas faire des caractères spéciaux ici, je mets des "pour tout" plutôt que des produits, des "il existe" plutôt que des sommes, etc, enfin je pense que vous savez traduire ça en une propriété de la théorie d'homotopie des types). En fait c'est une application du lemme 3.3.4 : "toute simple proposition est un ensemble". Or donc, (pour tout x de S1, base = x), c'est essentiellement isProp(S1) ; et isSet(S1) vaut (pour tous x et y de S1, pour toutes preuves p et q de x = y, (p =q)). Or ce dernier est faux, puisque contredit par Refl(base) et Loop dans (base = base). Si l'on veut être plus exact en restant dans la théorie, nous avons une fonction allant de (pour tout x de S1, base = x) dans isProp(S1) (étant donné x, y de S1, mon hypothèse me donne des preuves de (base = x) et de (base = y) que je peux combiner en une preuve de (x=y) ), une fonction de isProp(S1) dans isSet(S1) donnée par le lemme, une fonction de isSet(S1) dans (Loop = refl(Base)) (il s'agit de l'opérateur appliquant un habitant de isSet(S1) à (base, base, Loop, Refl(base)), et enfin une fonction de (Loop = Refl(base)) dans 0 (c'est l'hypothèse que Loop est non-trivial), composer le tout me donne une fonction de (pour tout x de S1, base = x) dans 0, soit ce que j'affirmais au-dessus. \o\ |o| /o/ Ici j'ai l'impression que l'on touche du doigt l'étrangeté des maths intuitionnistes. En fait, en logique classique, j'en déduirais qu'il existe existe un x dans S1 qui est différent de base. Sauf que je ne peux pas le faire en théorie des types, faute de me donner les moyen de construire un autre habitant de S1. J'ai vraiment l'impression qu'il existe d'autres points que ma base, mais il ne s'agit que d'un mirage et je ne peux saisir aucun de ces points. Je peux faire le tour du cercle (en utilisant Loop) et constater que je ne me suis pas contenté de rester au même endroit, sauf qu'il n'y a jamais eu d'autres endroits à parcourir pour en faire le tour. C'est extrêmement déroutant. Je suppose que c'est l'analogue de ce que vous disiez du R dans la vidéo précédente, qu'il est tellement continu qu'on ne peut pas le couper en deux pour séparer ce qui est plus grand de zéro de ce qui est plus petit. Ceci étant, j'en suis encore à essayer de comprendre réellement le lemme 3.3.4, à essayer de voir si je peux montrer ma propriété uniquement via des outils plus bas niveau que ce lemme, et surtout à essayer de me convaincre que je ne peux pas envoyer S1 dans 0. Bref, je commence à comprendre deux trois trucs qui sont sans doute élémentaires (je suis sûr que ça fait sourire tous les gens connaissant le domaine de voir que je suis fier de montrer une propriété aussi élémentaire sur S1), mais j'ai vraiment l'impression de rien panner. Entre autre, le lemme 3.3.4 est vraiment bizarre lorsqu'on le traduit en théorie de l'homotopie "classique" : "tout espace connexe (par arc) est simplement connexe" (le "par arc" me semble redondant, puisqu'en homotopie des types il n'y a aucune notion qui ne soit pas issue des chemins : évidemment que lorsque l'on traduit en homotopie "classique", parler d'une propriété P signifie toujours "P par arc"). J'ai l'impression que c'est la path induction qui donne tellement de possibilités de constructions de chemins, qu'il n'est plus possible d'envisager un espace connexe troué (...S1 se plaçant dans une catégorie bizarre où l'on sait montrer la non-connexité, mais on ne peut extraire qu'une composante connexe), mais visiblement l'univalence joue aussi un rôle dans la démonstration du lemme. Et surtout, en homotopie "classique", S1 n'est pas connexe OK, mais si je veux étudier les propriétés des chemins de base vers base, je me restreins à sa composante connexe ; visiblement en homotopie des types, ça ne marche absolument pas (ce qui ressemble le plus à la composante connexe de (base) : S1, c'est (somme pour x dans S1 des (base = x)) - un habitant de cet espace est un habitant de S1 muni d'un chemin de base vers x - , mais en passant de S1 à cet espace, Loop collapse sur la reflexion - le chapitre sur la path induction mentionne que l'on a dans cet espace une preuve de (base, Refl(base)) = (base, Loop) ; en somme, contrairement à l'homotopie classique, extraire une composante connexe en détruit les propriétés - ou plutôt, on ne sait pas isoler une composante connexe du reste de l'espace, si bien que la méthode pour tenter de le faire est tellement approximative qu'elle en détruit les propriétés). J'espère ne pas avoir écrit trop de conneries et vous félicite à nouveau pour votre excellent travail de vulgarisation (j'aurais absolument rien panné du livre sans vos explications initiales, même si j'en avais connu l'existence). :) En passant, je sais que beaucoup de gens se plaignent que vos vidéos sont trop compliquées ; et je sais qu'il faut que vous gardiez le contact avec votre public, ce qui ne sera possible que si vous continuez à faire aussi des vidéos plus accessibles. Dites-vous cependant que le fait de faire des vidéos de vulgarisation mais malgré tout de haut niveau, c'est ce qui vous distingue du reste, en somme ce qui donne une utilité à votre chaîne : des chaînes vulgarisant mais sans aller trop haut niveau, on en trouve déjà plein. Vous êtes en droit de me répondre "M. Le Roux, votre avis là-dessus aurait plus de valeur si les gens comme vous très intéressés par une chaîne comme la mienne la finançait" (il faut absolument que je le fasse).

[@Kaggan-zf7np]

Ce coup ci, je laisse tomber l'épisode hardcore car j'en suis encore à comprendre certains épisode de cette série. A+!

[@txia77]

J'ai découvert S4A grâce aux magies des maths de prépa... Même si je comprends pas toutes les épisodes, même parfois beaucoup je l'avoue, mais à chaque fois j'ai l'impression de voir l'envers du décors et surtout d'entre-apercevoir cette sensation d'intuition des maths (qui malheureusement fait défaut lors de nos cours de maths)... c'est ça que j'aime..

[@yassinesep7246]

J'essaye de comprendre tes episodes hein, mais là je suis perdu x)

[@anissamohib3750]

RATATOUILLE DU BLED pareil

[@dylanvellut]

je pensais que c'était des maths, mais les chiffres me manquent...

[@marycrowley5984]

Haha j'ai longtemps hésité a poster ce commentaire mais bon, vu que je ne suis pas la seule a suivre ses vidéos et n'avoir absolument rien compris a celle ci ^^.... C'est moi ou il nous parle en chinois ? Désolé >.>

[@nogadrama2595]

Ah, ce cliffhanger...hâte de voir la suite!!! Google se met à faire des ordinateurs quantiques, je sais pas si ça compte comme une machine de Turing, mais en tout cas ça fait un argument en plus pour la théorie de Church-Turing... D'ailleurs, est-ce que la théorie des types est compatible avec l'algorithmique quantique?

[@adfr1806]

J ai 16 ans et j’ai absolument tout compris jusqu’a 5:20. Pourtant j’aimerais bien tout comprendre mais j’ai bien peur que je n’ai pas toutes les notions. Petite question : l’ecole polytechnique fédérale de Lausanne propose des cours de mathématiques a raisonnements par l’absurde et des démonstrations avec les axiomes d’ensemble?

[@MJAjani1173]

prépa physique chimie... ah je croyais qu'on balançais les classes dans laquelle on est !

[@Fumeal]

Énorme travail et très bonne vidéo comme d'habitude !! Par contre j'ai rien compris et je sens que l'épisode hardcore va etre dur... (ça fait beaucoup trop de sous-entendu sexuel tout ça...)

[@AinexLeNoir]

Je trouve ça paradoxal de prétendre qu'une vidéo est très bonne sans n'y avoir rien compris.

[@Mindsway]

Je trouve ça paradoxal de n'avoir rien compris du tout

[@Killerdu67000]

Tous sa me rappelle beaucoup le principe des spécifications algébrique en informatique

[@cyrilleguedon5685]

Il faut des exemples concrets pour comprendre à quoi servent les théories. Dans les nombres et les infinis il y a des tas de curiosités dont on aurait jamais parlé sans Ramanujan. Par exemple il existe ces égalités presques parfaites: exp(π√427)=12³((7215+924√61)²-1)³+744 ou encore: exp(π√37)=64(√37+6)⁶-24-69(√37-6)⁶/16-271(√37-6)¹²/128. Il y en a une infinité, elles mettent en relation les nombres transcendants et algébriques, à quelle loi obéissent elles?

[@redswap]

Est-ce que tu feras une vidéo sur la définition de ce qu'est l'aléatoire ? Ça m'intéresserait...

[@mathislefebvre9721]

Même avec beaucoup de bonne volonté ça devient compliquer à comprendre là :/ Mais ça reste une super vidéo comme d'habitude :)

[@arthurblaser2268]

J'ai rien compris mais c'est bien fait, on vois que ilèy a du travail derriere c'est agreable.

[@augustinfrancotte3163]

Super vidéo ! Question par rapport au caractère aléatoire de la physique quantique, est ce qu'il n'a pas été démontré de manière rigoureuse qu'il n'existe pas de variables cachées explicatives: la violation des inégalités de Bell par l'expérience de Aspect ?

[@GrothenDitQue]

Francotte Augustin Ce qui a été démontré est l'inexistence de variables cachées *locales*, Lê précise bien que l'on ne sait pas quant aux variables *non locales*! ;)

[@augustinfrancotte3163]

Ah, merci pour cette précision ! Il est vrai que j'avais lu qu'il s'agissait bien d'une démonstration pour les variables cachées locales. Mais ces variables cachées globales ne pourraient elles pas violer des principes de la relativité générale ? Comme la vitesse de la lumière indépassable ...

[@GrothenDitQue]

Francotte Augustin Avec plaisir! Oui voilà. Ah alors il faut regarder mais, à mon avis, il ne s'agit là que d'une interprétation alternative de la mécanique quantique, mais qui ne résout néanmoins nullement les problèmes de compatibilité que celle-ci présente avec les mécaniques relativistes!... :/

[@Fine_Mouche]

il y a des phénomène qui peuvent dépassé la vitesse de la lumière sans violer les loi de la physique ... exemple : le cisaillement (le déplacement de l'intersection de 2 droites), le déplacement d'une ombre et d'autre que j'ai plus en tête

[@augustinfrancotte3163]

L'univers est en expansion accélérée, il se peut donc que la vitesse d'éloignement de certains points très distants dépasse la vitesse de la lumière. Seulement, s'il existe une force explicative globale à la mécanique quantique, il s'agirait d'information qui serait transmise instantanément d'un endroit à l'autre, c'est assez différent.

[@ledixiemedocteur8335]

Les entiers relatifs, c'est ce que l'on trouve sur ses relevés de compte ! Voilà une application des maths : la finance ! Blythe Masters, ancienne haut cadre de JP Morgan Chase, est à la base une mathématicienne formée à Cambridge.

[@antoine-lw5vg]

Quel est le lien avec le nom de la série : Infini ? J'ai l'impression qu'il y en a un, mais il est super abstrait. Quelque chose comme, le fait que finalement l'infini pose des problèmes, et la théorie des types ne laisse pas de place à des notions comme l'infini ?

[@samuelvidal3437]

La seule chose que je regrette c'est de ne pas pouvoir laisser plus d'un like. Je surkiff Bisous !

[@chkone007]

#PlatonicienFTW Pour info Gerard Berry a fait plusieurs colloque au Collège de France sur les preuves de programme, le lambda calcul, le pi calcule etc: www.college-de-france.fr/site/gerard-berry/_course.htm D'ailleurs le 1er truc qu'on fait pour des preuves de code/algo c'est de le transformer en langage fonctionnel (pour être Lambda pure) et là il y a plein de théorème (constructiviste :( ) applicable.

[@amineboujida1276]

Je pense toujours au fait que le sol accelere vers le haut si on suppose que ceci est vrai je tire une balle direct en haut par une kalach et donc la balle a la vitesse initiale communiqué par le kalach + la vitesse que lui communique l'acceleration de la terre apres le moment du tire on la nomme v0 selon votre hypothèse après que la balle retombe par terre c'est le sol qui y est monté et donc le sol dépasse la vitesse v0 (ce qui est normal puisqu il est en acceleration constante) + la vitesse initiale de la balle qui est de 750m/s soit 2 700 km/h , la distance terre lune de 358350 si on suppose que la vitesse de la terre est de 2700 km/h elle doit donc rencontrer la lune dans presk 135 heure (si on suppose que le temps s ecoule de la meme façon tout le long de la distance terre lune) et touut ça si on neglige le faut que la lune accelere aussi J'ai une grande confiance en einstein et je sais que oubien quelque chose va pas avec mon raisonnement oubien toi tu n'a pas su expliquer ce qu'einstein dit voudrais tu m'aider donc a comprendre ce qui s passe exactement et merci.

[@Abraccuda]

Coq qui a été développé par l'INRIA si je me trompe ?

[@sylvainpoirier4206]

Qu'y a-t-il donc de si extraordinaire dans les fondations univalentes : qu'il existe un plongement strict (non-isomorphique) de l'univers des mathématiques "classiques" dans l'univers des mathématiques univalentes ? Cela n'empêche nullement qu'il existe par ailleurs un autre plongement, de l'univers des maths univalentes dans l'univers des maths classiques, dans la mesure où les maths univalentes sont algorithmiques et que le concept d'algorithme est définissable en "maths classique". La seule "grande nouvelle" est qu'un tel second plongement ne saurait être l'exact inverse du premier. Bon et après ? Avoir une théorie dans laquelle toutes les fonctions sont continues ? En maths classique on a néanmoins le droit de ne s'intéresser qu'aux ensembles des fonctions continues. Il y a même encore mieux: pour les gens qui ne se sentiraient pas confortables avec les fonctions continues dont la convergence serait plus lente que 10^10^....10^10/log(log(log.... log(1/x)...))) (avec n logs et n dix) pour un quelconque n, les maths classiques nous laissent même le droit de définir l'ensemble des fonctions continues qui ne sont sujettes à une telle lenteur de convergence en aucun point, et de ne travailler qu'avec cette ensemble si ça nous chante !!! A part ça, ce que pour l'instant je retiens de cette histoire, donc, comme avantage principal des maths univalentes sur les maths classiques c'est son explication de comment gagner des concours de programmation des calculs du plus grand nombre possible de groupes d'homotopie. Cependant, aussi beau que cela soit, j'ai du mal à voir à quoi d'autre ça pourrait servir. Sans avoir étudié précisément l'interaction electrofaible, je conçois que la brisure de l'interaction électrofaible en électromagnétisme+ interaction faible puisse fair appel à un ou deux groupes d'homotopie ; de même pour l'interaction forte. Je suis même prêt à envisager que la théorie des supercordes, dont le rapport avec la physique reste totalement spéculatif, utilise des groupes d'homotopie en pagaille. Néanmoins je reste perplexe: quel rapport sérieux tout cela peut-il avoir avec la question du... fondement des maths, à savoir, éventuellement plus précisément, la question de comment serait-il mieux de démarrer les maths en première année universitaire (libre à chacun de refuser de s'intéresser à cet aspect particulier de la question générale des fondements) ? En effet j'ai une philosophie suivant laquelle les ordinateurs devraient être au service des humains et non l'inverse, de sorte que la question de savoir quelle est la plus puissante façon de programmer les ordis ne devrait pas asservir notre cerveau. Du moins pas trop souvent... Cependant il y a bien des choses intéressantes à chercher du côté de la logique en rapport avec le réel, précisément la physique, mais autrement : voir plus de commentaires dans ma page settheory.net/intro

[@lionelguez4814]

rien compris mais passionnant

[@hadydia6727]

tout le monde fustige Eddy Malou mais lui aussi ... xD

[@user-ss5oo4rs7f]

Désolé, je n'ai pas compris ce qu'est un "type", et donc l'équivalence entre deux types.

[@leschatsfontdix6246]

Merci,

[@francklevequeww9839]

ce jeune et intèssend,maime si je suis malade.lerous setphane.

[@demonceaukarldemonceau5241]

bonjour a toi je cherchais axiume et je suis tomber sur toi , j'ai éccouter la vid jsqu au bout ça me fais pense a la matière noir le point

[@sylvainpoirier4206]

Sur l'indéterminisme quantique : la réponse par la théorie bohmienne pose beaucoup de problèmes, dont notamment le fait que... elle commet un gros hors sujet vis-à-vis de ses propres prétentions, son exploit effectif consistant bien moins à réussir à se conformer aux critères du déterminisme, qu'à noyer le poisson en redéfinissant le label "déterministe" pour le vider de l'essentiel de sa signification logique en sorte de pouvoir étiqueter par ce vernis une théorie dont la différence avec la MQ standard n'est pas vraiment claire (puisqu'elle donne les mêmes prédictions !), de sorte qu'il n'est pas clair en quoi elle serait effectivement "déterministe" en particulier. Voir mon argumentaire détaillé en anglais : settheory.net/Bohm (J'avais déjà répondu sur la théorie bohmienne en réponse à Damien Aubert en commentaire de kzbin.info/www/bejne/iJuWm4etZ6mrjrM ) Sur la modélisation par les processus de Markov : effectivement il semble que les prédictions de la MQ soient traduisibles en cela, cependant, à part le fait qu'aucune loi physique ne vient préciser les circonstances suivant lesquelles les tirages aléatoires doivent être insérés (à savoir la décohérence, notion émergente), une telle traduction se présente en pratique comme "pas naturelle", les mesures de complexité de part et d'autre n'étant nullement compatibles. Notamment, comment qualifier d'algorithmique un processus de Markov dont chaque étape se fait suivant une certaine probabilité dont on peut donner une valeur approximive par un calcul fini mais dont la valeur exacte nécessiterait un temps de calcul infini ? j'ai raconté cela plus longuement dans mon texte settheory.net/fr/dualisme-esprit-math

[@PierreYvesStrub]

C'est un peu dommage de réduire la théorie des types à l'axiome d'univalence...

[@Fine_Mouche]

MDR pour les boucles j'ai crée un objet mathématique que j'ai nommé pour le moment "chemin perdu" ou "chemin-polygone-étoile" où les boucles on leur importance et non pas la même signification qu'un aller-retour ou rien faire. : Je m'étais d'abord concentré sur le trajet d'un mobile autour d'un polygone si à chaque sommet il avait le droit d'avancer ou reculer. Mais il ne fallait pas qu'il reste bloqué à faire un aller-retour d'un sommet à un autre indéfiniment. j'ai donc chercher à établir des règles. j'ai tester mes règles sur plusieurs polygone mais cela devenais compliquer (à partir du pentagone) et j'ai chercher à changer de point de vue. Je suis dont passer de polygone à une droite segmenté et vue que certaine règle n'allais pas et que ma conjecture était fausse. Je me suis poser des questions sur la droite à 2 segment (ou un un segment en 2 parties / coupé en 2) et je suis arrivé sur l'étoile, devais-je rajouter une flèche ? j'avais testé les 2 hypothèses et cela m’amenai sur quelque paradoxe / incohérence mais fini par faire le liens entre polygones et étoiles. Maintenant que j'ai 3 représentation je dois me décider sur quel règles appliquer au cheminement de mon mobile pour avoir des trajet intéressant à étudier. Ce qui suit sont ldes photos de mes feuilles que j'ai poster à mon père sur FB, (S'ils sont de mauvaise qualités, illisibles, trop brouillon, je les reprendrais, re-rédigerais) : www.noelshack.com/2017-08-1487634990-chemin-perdu.jpg (1ere feuille, avec une conjecture sur la marge qui est sans doute fausse) www.noelshack.com/2017-08-1487635229-segment-et-decouverte-polygone.jpg (autre représentation qui m'a permis d’avancer) www.noelshack.com/2017-08-1487635400-conjecture-fleche-oui-ou-non.jpg (une question qui ma permis de trouver une 3eme représentation) www.noelshack.com/2017-08-1487635060-chemin-vers-polygone-vers-etoiles.jpg (la synthèse des 3 représentations, le lien entre les 3 représentation) www.noelshack.com/2017-08-1487635038-contre-sens.jpg (des contre sens, configuration plus ardue à comprendre) www.noelshack.com/2017-08-1487635193-pb.jpg (un problème, questionnement) www.noelshack.com/2017-08-1487635199-pb-resolu.jpg (le problème en parties résolue) Ainsi la Boucles = Cercles de ta vidéo pourrais être le segment à 0 parties ( ou la droite à 0 segment)

[@cyrilcohen3233]

1. RIP Vladimir Voevodsky... 2. La motivation de la vidéo est ratée : le quotient N²/R (avec R (p₁, n₁) (p₂, n₂) = (p₁ + n₂ = p₂ + n₁)) est tout a fait "constructif", soit parce que A. les higher inductive types (HIT en HoTT) permettent de former des quotients de manière constructif (pourvu que l'on ait un modèle constructif), soit parce que B. ce quotient là en particulier est un quotient effectif e.g. il existe un représentant canonique (p, n) pour chaque classe d'équivalence (grâce à la contrainte p = 0 ou n = 0 qui amène à une unique solution). Enfin, il n'est absolument pas nécessaire de faire un quotient pour obtenir une représentation constructive de Z : N + N suffit (union disjointe ou type somme en théorie des types). 3. HoTT reste intéressant, et effectivement π₁( S¹) = Z est un exemple emblématique, mais également la possibilité de raisonner modulo isomorphisme (grâce au Structure Identity Principle). En tout cas je ne sais pas qui aura compris le contenu de la vidéo mais chapeau pour l'essai.

[@francklevequeww9839]

je suis un mèque qui ètait, bon en matte, mes jai atrpè;une locopathie vasculaire.je dois penser à une chose a la foie et des jen pa trè sinpa ce foute de moi mes aaaaa-= a jarive aussi a aaa et je ces pa comment je fai et jai besoin dinde jètè otdidacte et pourtant jai pa hu de chance a l'ecole/dctrsten.et etonament je compend mes je narive plus a retenire, 2plus je suis insominiaque;et mon sèrveaux pare en balade;padon pour les faute je feser plus cete maladie me cose boucoup de soufrence!je te trouve intèsent.merçi toi,je crois a la tèorie aux trous de verre.

[@arielorthmann4061]

Salut ! J'espère que quelqu'un lira ce commentaire et pourra m'aider. J'ai un problème. Je veux qu'un événement se produise, quand je lance un algorithme/machine/quoi que ce soit, avec 100% de certitude, mais peu importe après combien de temps après que je l'ai demandé. Ça peut être après 30 minutes, 5 secondes ou 200 ans. Tant que ça se produise, avec 100% de certitude, tout va bien. Maintenant, j'ai une machine qui, quand je la lance, à chaque seconde, a 1 chance sur 2 que l'événement se produise. Cette machine respecte-elle les conditions ? J'ai trouvé deux approches qui semblent juste mais dont contradictoires, je me demande laquelle est juste et laquelle est fallacieuse : On peut représenter la probabilité que l'événement ne se produise pas par 1/2^N secondes. Donc, avec une infinité de temps et de secondes, la probabilité sera 1/2^♾️=?0. Donc, avec une infinité de temps, ça marche à tout les coups. Mais du coup, s'il faut une infinité de temps avant que ça marche (à coup sûr), ça veut dire que ça échouera pendant une infinité de temps, donc que ça ne marchera jamais, non ? Voilà j'espère que la formulation du problème est compréhensible. Merci d'avance de prendre le temps de me lire 😄!

[@chromalucario7939]

Je ne suis pas du tout un spécialiste mais je comprends "avec une infinité de temps, ça marche à tous les coups" comme à chaque lancer, il existe n dans IN tel que le lancer réussisse. Ainsi, après une infinité de temps, les n lancer auront été atteints et donc le lancer réussira. Mais si on fait un nombre m fixé de lancer, quelque soit m il existera toujours des n>m donc il faut bien faire une infinité de lancer pour être certain que le lancer réussisse mais en faisant une infinité de lancer, on arrivera au lancer n qui réussira.

[@j9dz2sf]

En y réfléchissant avec l'idée une preuve formelle (dans la tête), la réponse est non. L'infini, on ne peut pas le représenter. On peut juste dire "∀ t" où "t" est un temps limite que l'on s'impose. Ça peut être n'importe lequel mais il en faut un. Quel temps "t" proposes-tu ? Vas-y, dis-en un. Je te répondrai alors que la probabilité que l'événement ne se produise pas n'est pas nulle. Aussi petite que tu veux mais pas nulle. Tu pourras prouver ∀ ε>0, ∃ t, P(t)

[@renaudg9311]

Bien fait d'étudier la physique plutôt que les maths pures si c'est ça leur futur... Ça me passionne et intéresse absolument pas (d'ailleurs heureusement que c'est la fin de la série ^^).

[@Fine_Mouche]

Il n'y a pas que cela en maths, il y plein de domaines, Je dirais qu'il y a autant de domaines que de mathématicien XD

[@G4-Dylan]

de la même manière une droite peut représenter un cercle, sa se tiens pas... et la boucle base->base n'a pas lieu car ya pa la même direction

[@tctrainconstruct2592]

400th like

[@sebastiendesbordes4823]

MDR pour les boucles j'ai crée un objet mathématique que j'ai nommé pour le moment "chemin perdu" ou "chemin-polygone-étoile" où les boucles on leur importance et non pas la même signification qu'un aller-retour ou rien faire. :

[@sebastiendesbordes4823]

Je m'étais d'abord concentré sur le trajet d'un mobile autour d'un polygone si à chaque sommet il avait le droit d'avancer ou reculer. Mais il ne fallait pas qu'il reste bloqué à faire un aller-retour d'un sommet à un autre indéfiniment. j'ai donc chercher à établir des règles. j'ai tester mes règles sur plusieurs polygone mais cela devenais compliquer (à partir du pentagone) et j'ai chercher à changer de point de vue. Je suis dont passer de polygone à une droite segmenté et vue que certaine règle n'allais pas et que ma conjecture était fausse. Je me suis poser des questions sur la droite à 2 segment (ou un un segment en 2 parties / coupé en 2) et je suis arrivé sur l'étoile, devais-je rajouter une flèche ? j'avais testé les 2 hypothèses et cela m’amenai sur quelque paradoxe / incohérence mais fini par faire le liens entre polygones et étoiles. Maintenant que j'ai 3 représentation je dois me décider sur quel règles appliquer au cheminement de mon mobile pour avoir des trajet intéressant à étudier.

[@sebastiendesbordes4823]

Ce qui suit sont ldes photos de mes feuilles que j'ai poster à mon père sur FB, (S'ils sont de mauvaise qualités, illisibles, trop brouillon, je les reprendrais, re-rédigerais) : www.noelshack.com/2017-08-1487634990-chemin-perdu.jpg (1ere feuille, avec une conjecture sur la marge qui est sans doute fausse) www.noelshack.com/2017-08-1487635229-segment-et-decouverte-polygone.jpg (autre représentation qui m'a permis d’avancer)

[@sebastiendesbordes4823]

www.noelshack.com/2017-08-1487635400-conjecture-fleche-oui-ou-non.jpg (une question qui ma permis de trouver une 3eme représentation) www.noelshack.com/2017-08-1487635060-chemin-vers-polygone-vers-etoiles.jpg (la synthèse des 3 représentations, le lien entre les 3 représentation)

[@sebastiendesbordes4823]

www.noelshack.com/2017-08-1487635038-contre-sens.jpg (des contre sens, configuration plus ardue à comprendre) www.noelshack.com/2017-08-1487635193-pb.jpg (un problème, questionnement) www.noelshack.com/2017-08-1487635199-pb-resolu.jpg (le problème en parties résolue) Ainsi la Boucles = Cercles de ta vidéo pourrais être le segment à 0 parties ( ou la droite à 0 segment) Moins

[@xXdarkangel67Xx]

cinquième

[@sassou0]

J'apprend coq à l'école mais pas dans ce sens là :o

[@arthurbelleville3641]

Second

[@misnik1986]

s'il vous plait, soyez un peu clair essayez de faire beaucoup de dessin et de geometrie car c totalement incomprehensible

[@ouraN2O]

Quatrième

[@yannisdsv3139]

troisieme

[@ouraN2O]

Lol

[@fefedu6890]

First

[@arthurreitz9540]

Sur une video de math il faudrait plutôt mettre "zéro-ième".

[@christophem6373]

Sauf si on fait bien la différence entre ordinaux et cardinaux... ;-)

[@jeansartre6756]

cinquième